Natural Number Game

adam.math.hhu.de · 655 words · saved by 4 readers

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

A repository of learning games for the proof assistant Lean (Lean 4) and its mathematical library mathlib Translators needed We are actively looking for volunteers to translate the existing games to languages not yet available, in particular for the Natural Number Game and Robo/Scribble. If you are interested, please get in touch. See these guidelines to get an idea of the effort involved. Natural Number Game The classical introduction game for Lean. In this game you recreate the natural numbers N\mathbb{N} from the Peano axioms, learning the basics about theorem proving in Lean. This…

Natural Number Game

saved by

related reading