The natural number game

The natural numbers

The natural numbers ℕ are one of the most fundamental entities in mathematics. They carry the algebraic operations of addition and multiplication, which certain various properties: associativity, commutativity, neutral elements, etc. Addition and multiplication are also compatible in the sense that addition distributes over multiplication. Apart from these algebraic operations we also have a linear order on ℕ that is compatible with both addition and multiplication.

At the heart of the natural numbers lies the successor function n ↦ n + 1, which leads to the formalization of the natural numbers via the Peano axioms:¹ the natural numbers consist of a set ℕ and a function ν from ℕ into itself, called the successor function, such that the following properties are satisfied:

1. (Existence of zero.)
	There exists an element <span class="math">0</span> of <span class="math">ℕ</span>.

2. (Successor function.)
	The successor function <span class="math">ν</span> is injective and there exists no natural number whose successor is <span class="math">0</span>.

3. (Principle of induction.)
	Let <span class="math">P</span> be a statement about natural numbers such that

	- <span class="math">P(0)</span> is true, and
	- whenever <span class="math">P(n)</span> is true, <span class="math">P(ν(n))</span> is also true.

	Then <span class="math">P(n)</span> is true for every natural number <span class="math">n</span>.

The game

The natural number game is a puzzle game developed by the mathematician Kevin Buzzard in which the natural numbers are built up from scratch. It starts off with only the Peano axioms and then introduces increasingly complex theorems about natural numbers throughout the game. Each new theorem has to be deduced from the previous ones, so that the player builds up an ever-growing list of known theorems and thus usable tools with each completed level.

The game uses the theorem prover Lean (via the Lean Game Maker) to make it possible for the player to derive a new theorem from the previous ones. The game is meant as a soft introduction to Lean, so no previous knowledge of it is needed to play. Only a few Lean commands are needed for the entire game, and these are slowly introduced throughout. (The game runs in the browser via JavaScript and does not require a local installation of Lean.)

I’ve played through the game over the last few days and found it quite enjoyable. I had never before actually constructed the natural numbers from scratch, though I was aware of how it could be done. It also hasn’t been done in any lecture I ever attended, probably because it seems annoying and not worth the time. I found that the natural number game does a good job of dispelling this preconception: There has clearly been going a lot of work into the design and pacing of the levels: I always felt that I was making progress.

I’d definitely recommend every mathematician (and every computer scientist) to try out the natural number game. My personal solutions to the game can be found on GitLab. In the coming days I’ll probably familiarize myself more with Lean by trying out the Lean maths challenges.

TL;DR: Check out the natural number game, it’s pretty nice.