Lean Game Server
Prove math theorems level by level in the Lean language
The Lean Game Server hosts browser games where each level is a theorem to prove in Lean 4, a programming language and proof assistant. The best known is the Natural Number Game: you build the natural numbers from scratch and prove facts like 2 + 2 = 4 and x + y = y + x using tactics such as rw and induction. Lean checks every step and shows what is left to prove.
Free · No login · Browser · Beginner
About Lean Game Server
It trains formal reasoning and the basics of an interactive theorem prover. Other games on the server cover logic, set theory, linear algebra and real analysis.
It suits curious programmers and maths students; no prior Lean is needed. It is free and open source, with no account. Progress is saved only in your browser's local storage, so clearing site data erases it.
Made this game? Claim it →
Tips and discussion
No tips yet.
Sign in to share a tip.