Natural Number Game
In this game, we will build the basic theory of the natural numbers {0,1,2,3,4,...} from scratch. Our first goal is to prove that 2 + 2 = 4. Next we'll prove that x + y = y + x. And at the end we'll see if we can prove Fermat's Last Theorem. We'll do this by solving levels of a computer puzzle game called Lean. Learning how to use an interactive theorem prover takes time. Tests show that the people who get the most out of this game are those who read the help texts like this one. To start, click on "Tutorial World". Note: this is a new Lean 4 version of the game containing several worlds which were not present in the old Lean 3 version. A new version of Advanced Multiplication World is in preparation, and worlds such as Prime Number World and more will be appearing during October and November 2023. Click on the three lines in the top right and select "Game Info" for resources, links, and ways to interact with the Lean community. Tutorial World 1 2 3 4 5 6 7 8 Power World 1 2 3 4 5 6 7
Explore this link on the map →