The Natural Number Game

The Natural Number Game is an online exemplar of the theorem-proving software Lean and the development of mathematics from its very postulates. The player of this game is tasked with using some basic axioms and previously-proven results to inductively prove new mathematical theorems in a perfectly rigorous, verifiable way. The game was developed by Kevin Buzzard and Mohammad Pedramfar.

This blog post was written to help the curious reader start playing the game and become comfortable with the underlying topics and basic commands used throughout the game. I cover "spoilers" for the first few "worlds."

Lean

For context, Lean is an open-source theorem prover/proof assistant in the form of a programming language based on a higher-order typed lambda calculus called the calculus of constructions with inductive types, began in 2013 by Leonadro de Moura. It's not vital to understand what each of these qualities means precisely, but it is important to understand Lean's impact on formalizing mathematics.

Lean is primarily used for formal verification, a process of mathematically proving the correctness of software and hardware systems by providing a platform for rigorous mathematical reasoning and verification. Lean-verified software or hardware systems are high-assurance and certainly more reliable.

In the context of the Natural Number Game, Lean serves as the user's proof assistant, enabling the user to both write and check complex mathematical proofs interactively.

Mathematical Setting

The mathematical model whose theory we study is that of the natural numbers with some basic principles of induction and the Peano Axioms.

An example of an early task for the player is to prove the principles of mathematics usually taken for granted: e.g., why is addition commutative? i.e., why does x + y = y + x?

Every level in the Natural Number Game involves proving a theorem. The goal of the level's theorem will be in the form of a mathematical statement preceded by the symbol ⊢. Within a level, our process will involve employing various tactics to manipulate the starting expression and ultimately close/prove our goal.

Proofs consist of employing tactics, or syntactic rules which help Lean manipulate and/or compare mathematical expressions. The two most basic tactics employed in the game include:

• refl: reflection. This tactic "proves" any expression of the form expr = expr. This is the formal way to instruct the Lean proof checker: "Both sides of the equals sign are identical, so conclude that the equality is true." This rule won't work if the two sides of the equals sign are mathematically equal but not syntactically identical: for instance, while 2x = x + x is true for any natural number x, the reflection tactic will not be able to do anything here, because the left hand side is not identical to the right hand side. Calling the reflection tactic is as easy as typing refl, on its own line. Lean will compare the expressions on either side of the equals sign and conclude "true" if and only if the two sides match.
• rw: rewrite. This tactic "substitutes" a mathematical expression by another expression to which it is equal. This tactic requires an argument stating which equality/equivalence to reference in order to perform the substitution. For instance, if we have a rule h which states h: y = 2 * x, and our goal is to prove that y + 5 = 2 * x + 5, we will first instruct Lean to rewrite y as 2 * x by typing rw h,. This instruction can be read aloud as "Anywhere where you see the left hand side of h, replace it with the right hand side of h." The result of this instruction will be 2 * x + 5 = 2 * x + 5. To finish this example, we simply call reflection refl, on the following line to instruct Lean to compare the left hand and right hand sides of the equality and notice that they are syntactically identical, concluding the result.

The predefined type mynat in Lean offers a predefined term 0 : mynat interpreted as the natural number zero, as well as a predefined function succ : mynat → mynat interpreted as the successor function, or the function which outputs the next natural number after its input. Finally, mynat also obeys mathematical induction, or the principal that if for predicate (i.e., a true/false statement about the natural numbers taking a natural number as input) P it is true that:

• P is true for 0, and
• Whenever P(n) is true this implies P(succ(n)) is also true,

then P is true for all natural numbers. This principle of mathematical induction is likened to dominoes toppling: if the first domino in a line of dominos falls, and the dominos are all arranged such that each falling domino knocks over the next one, then all of the dominos will eventually fall. Together with recursion to define certain mathematical operations, these assumptions constitute the Peano axioms of the theory of the natural numbers. For instance, our assumption that 0 is a natural number counts as an axiom. The fact that there exists a successor function succ implicitly necessitates a few axioms.

Peano's claim was not only that his axioms characterize the natural numbers, but also that one could use these axioms within classical logic to develop many features of the natural numbers such as the rules underlying addition, multiplication, etc. In this way, the Natural Number Game aims to show just how far the Peano axioms take us, as well as which ones are necessary to deduce particular theorems about the natural numbers.

Tutorial World

We have certain other tactics at our disposal, such as add_zero which simplies anything of the form x + 0 to x using the axiom about addition by zero. In the syntax of Lean, this looks like

add_zero (x : mynat) : x + 0 = x

Another axiom coded into Lean as a tactic is written as follows:

add_succ (x y : mynat) : x + succ(y) = succ (x + y)

We read this in plain English as "In order to add x with the successor of y, simply take the successor of the sum of x and y". This provides us an inductive way to figure out how addition works for larger inputs.

At the fourth and final stage of the Tutorial world, we are tasked with proving the Lemma

lemma add_succ_zero (a : mynat) : a + succ(0) = succ(a) :=

i.e.,

\[\text{\textbf{Lemma}: For any $a \in \mathbb{N}$ we have $a + \operatorname{succ}(0) = \operatorname{succ}(a)$}.\]

We know that the add_succ rule should tell us that a + succ(0) is equivalent to succ(a + 0), and add_zero should simplify a + 0 to a. These two steps should be enough to bring us to a simple conclusion by calling the reflection tactic:

-- goal : a + succ 0 = succ a
rw add_succ,
-- goal: succ(a + 0) = succ a
rw add_zero,
-- goal: succ a = succ a
refl,
-- goal: complete

Addition World

In order to prove the following theorem:

zero_add (n : mynat) : 0 + n = n

we will employ a new tactic: induction. While it is true that x + y = y + x, we have not yet proved that, so zero_add will be our first step towards proving the commutativity of addition. Moreover, while add_zero was a Peano axiom, zero_add need not be, because we can already prove it from the existing axioms. Employing the induction tactic will open two goals: the first to prove a base case, the second to prove an inductive step. Suppose our goal is ⊢ 0 + n = n: let's begin our proof with the line induction n with d hd, where n is the natural number referenced in the goal; d is name we'll give to the inductive step case: assuming true for d, prove the same for succ(d); and hd is the name we give to the inductive hypothesis that 0 + d = d. Then the resulting context will ask two goals:

2 goals
⊢ 0 + 0 = 0
 
case mynat.succ
d : mynat,
hd : 0 + d = d
⊢ 0 + succ d = succ d

We work on the top goal first by convention: a simple application of add_zero and refl should solve this:

-- goal: 0 + n = n
induction n with d hd,
-- goal: 0 + 0 = 0
rw add_zero,
-- goal: 0 = 0
refl,
-- goal: 0 + succ d = succ d

To proceed with the second goal which automatically queued up after completing the first goal, we pause to think: all we know is that hd provides the assumption 0 + d = d. How can we use this equality to prove the same for d's successor? We can bring addition inside the successor by the theorem add_succ, giving us succ(0 + d) on the left hand side. Aha! The inductive hypothesis can rewrite 0 + d to be d, resulting in the left hand side matching the right hand side, so reflection to finish off:

-- goal: 0 + n = n
induction n with d hd,
-- goal: 0 + 0 = 0
rw add_zero,
-- goal: 0 = 0
refl,
-- goal: 0 + succ d = succ d
rw add_succ,
-- goal: succ(0 + d) = succ d
rw hd, 
-- goal: succ d = succ d
refl,
-- goal: complete

The rest of Addition World employs these three tactics refl, rw, and induction to prove many more theorems, including the commutativity of addition and more.

The game introduces a useful tool to automate the proofs of results that would require a lot of simple manipulations for a human to bear: the simp tactic. Imagine having to show (((a+b)+c)+d)+e=(c+((b+e)+a))+d by hand writing every application of associativity or commutativity. It'd be a simple yet tedious task. The simp tactic employs AI-reasoning to close the goal by judiciously applying add_comm and add_assoc. This is accomplished as shown below:

instance : add_comm_monoid mynat := by structure_helper
example (a b c d e : mynat) :
(((a+b)+c)+d)+e=(c+((b+e)+a))+d := begin
  simp
end 

Function World

This world introduces four new tactics appropriate for proving results about functions: exact, intro, have, and apply, as well as a new type of goal. In this world, rather than prove theorems, our goal is to simply construct a term of a provided type, or an element of a provided set, written: ⊢ X. For example, Function World Level 1 begins with the context

P Q : Type,
p : P,
h : P → Q
⊢ Q

Achieving the stated goal is intuitively simple: simply apply h to p and get an output h(p) : Q. In Lean, we write:

-- goal: Q
exact h(p),
-- goal: complete

The exact tactic will take any formula to produce a term of some type and instruct Lean to check that the computed term is of the type called for in the goal.

In Level 2, our context is simply ⊢ mynat → mynat. This can be read aloud as "demonstrate any function with input of type mynat and output of type mynat." We begin by hailing into existence an arbitrary term of type mynat using the tactic intro. Lean will know that you wish to introduce a term from the domain type of the function. The goal then reduces to demonstrating a term of the codomain type of the original function. Because the domain and codomain were of the same type, finishing is as easy as calling exact on this arbitrary natural number.

-- goal: mynat → mynat
intro n,
-- goal: mynat
exact n,
-- goal: complete

In Level 3, our context is

P Q R S T U : Type,
p : P,
h : P → Q,
i : Q → R,
j : Q → T,
k : S → T,
l : T → U
⊢ U

The have tactic allows us to define an element of a particular type that appears in the middle of a calculation. For example, in this level, we could follow one of two solution methods: the first is direct:

-- goal: U
exact l(j(h(p))),
-- goal: complete

The second method is to keep track of the intermediate types:

-- goal: U
have q := h(p),
-- goal: U
have t: T := j(q),
-- goal: U
have u := l(t),
-- goal: U
exact u,

Finally, in Level 4, we learn of a third method to solve this problem using a different tactic: apply. This command helps us construct a path backwards from U to T to Q to P. We read apply l, as "to construct a term of type U, it would suffice to produce a term of type T, since l is a function of type T : U."

The full solution would look like:

-- goal: U
apply l, 
-- goal: T
apply j,
-- goal: Q
apply h,
-- goal: P
exact p,
-- goal: complete

The rest of the Function World uses these tactics to explore a few key ideas to the theory of functions in type theory.

Conclusion

There are many more worlds to play through, but part of the fun of the game is figuring them out for yourself! Best of luck!