This is a game about the natural numbers, which are the numbers {0, 1, 2, 3, ...}. It is based on this blog post but takes things a lot further.
The idea of the game is to teach you what actually goes into the proofs of all the statements about natural numbers which are presented to us as children and which we are told are "obvious". Examples of such statements are: a + b = b + a, or a * (b + c) = a * b + a * c.
If one uses a "geometric" and informal definition of addition, such as "a + b is the number of marbles you have, if you have a marbles in one hand and b in the other", then statements like a + b = b + a do become obvious. However, such a definition of addition is not appropriate for a computer. Our job in this game is to convince a computer that statements such as a + b = b + a are not just "obvious", but actually have proofs.
In this game, we start with the natural numbers and the principle of mathematical induction, and induction is the main tool that we will be using. If you are already happy with the principle of mathematical induction then hopefully you will be able to make some progress playing this game, and it might even teach you more about what the principle is.
Computers are currently being taught mathematics by mathematicians, and this game will give you some idea about how one has to think about mathematics in order to teach it to a computer. Computer scientists would like to teach difficult modern research mathematics to a computer, but this is currently extremely hard to do because computers find it very hard to read mathematics written by humans, even with recent advances in machine learning and AI. This is a big stumbling block in training computers to become brilliant mathematicians. The natural numbers game teaches you a language that computers find much easier to understand. The language we will be using is called Lean. Lean is a piece of free and open-source software developed by Leonardo de Moura at Microsoft Research.
- docs: compiled game files.
- experiments: possible future levels, e.g. primality, factorials, binomial coefficients, gcd, congruence.
- locale: translation files.
- src/game: Lean code for the worlds in the game, plus some LaTeX used to generate the diagrams because it was easier than figuring out how to make a LaTeX diagrams package work in this set-up.
- world1: Tutorial World
- world2: Addition World
- world3: Multiplication World
- world4: Power World
- world5: Function World
- world6: Proposition World
- world7: Advanced Proposition World
- world8: Advanced Addition World
- world9: Advanced Multiplication World
- world10: Inequality World (17 levels so far, but more have been written)
- src/mynat: definitions of the naturals, addition, multiplication, exponentiation and <=. These files are never seen by the user.
- src/tactic: modifications of the tactic framework (meaning that rw and induction and a couple of other things behave slightly differently -- see TECHNICAL.md for more explanation of this) and the definition of
structure_helper, a tactic which attempts to fill fields of a class by attempting to define fieldFwithmynat.F. - compile.sh, run_locally.sh: local scripts which run on a computer to compile and run the code locally.
- game_config.toml: settings file for Lean game maker (the graph of the game).
- leanpkg.toml: settings file for this Lean project.
- LICENSE: Apache-2.0 License.
Click on the above links to each world and see the lean files.
See TECHNICAL.md.
See WHATS_NEXT.md.
- Lean stuff: Kevin Buzzard. Find Kevin on the Zulip Lean chat or Twitter at @XenaProject.
- Computery stuff: Mohammad Pedramfar. See in particular Lean game maker.
Bulhwi Cha, Minju Kim, and Seongwoo Shim.