Maths in a Minute: Coding with Lean
Proof assistants are ways of making sure that there are no mistakes in a mathematical proof by making them rigorous. Let’s look at how proof assistants actually work. We are going to prove that if we have two integers a and b, then $(a+b)^2 = a^2 + 2ab + b^2$. (Unfortunately, it doesn’t equal $a^2+b^2$, as is sometimes called the Freshman’s dream.)
With pen and paper, the proof would be:
$(a+b)^2 = (a+b)(a+b)$
$=a(a+b)+b(a+b)$
$=aa+ab+ba+bb$
$=aa+ab+ab+bb$
$=aa+2ab+bb$
$=a^2+2ab+b^2$
There are many different proof assistants such as Isabelle, Rocq, Agda, but for our example, we will be using a proof assistant called Lean.
To prove this elementary result in Lean, we would begin by importing the libraries that contain the relevant theorems for our proof. In our case, it turns out that the relevant theorems are in packages called Mathlib.Data.Int.Basic and Mathlib.Algebra.Ring.Basic. The theorems that we will be using are
| Name of Theorem | What it says |
| pow_two | $x^2 = x \times x$ |
| mul_add | $x \times (y+z)=x \times y+x \times z$ |
| add_mul | $(y+z) \times x=y \times x+z \times x$ |
| mul_comm | $x \times y=y \times x$ |
| add_assoc | $(x+y)+z=x+(y+z)$ |
| two_mul | $2 \times x=x+x$ |
These are all quite basic results that have been derived for integers from the Peano axioms and are stored in Mathlib, a GitHub project that contains all completed work done on LEAN.
So, we begin with
import Mathlib.Data.Int.Basic
import Mathlib.Algebra.Ring.Basic
theorem int_square_expansion (a b : ℤ):
(a+b)^2 = a^2 + 2 * a * b + b^2 := by
So far, all we’ve done is to import the relevant libraries and to state the theorem that we want to prove. Now we will repeatedly use a tactic called rewriting. Essentially, what we will do is to rewrite the left-hand side of the theorem (a+b)^2 by employing the theorems that we imported. To employ the tactic rewriting, we just write rw[relevant theorem]. Beneath each line of code, the current state of the left-hand side of the equation will be written.
rw [pow_two]
(a+b)*(a+b)
rw [mul_add]
(a+b)*a + (a+b)*b
rw [add_mul]
a*a + b*a + a*b +b*b
rw[mul_comm b a]
a*a + a*b + a*b + b*b
Note that we specifically chose the b and a to be swapped in our code to stop, say, the a and the a being swapped, which wouldn’t achieve much.
rw[pow_two, pow_two]
a^2 + a*b + a*b +b^2
Now it turns out that the way that Lean reads this is as (((a^2 + a*b) + a* b) +b^2). That is, we have nested brackets. So, if we want to apply our two_mul rule, we need to rearrange the brackets a bit using:
rw[add_assoc (a^2) (a * b) (a * b)]
a^2 + (a*b + a* b) +b^2.
Again, we have chosen the specific elements of our equation that we wanted to apply the rewrite to.
rw[← two_mul]
a^2 + 2*a*b +b^2.
The use of the backwards arrow just means that we are turning a*b + a*b into 2*a*b, rather than turning 2*a*b into a*b + a*b.
rfl
Finally, we finish our code by writing rfl, short for reflexive, just to mean ‘now the left-hand side equals the right-hand side, so we are done’.
It might still seem difficult to wrap your head around Lean coding. When I was trying to understand it, the best resource that I found was the Natural Number Game, made by Kevin Buzzard. You can have a play yourself; the first world will show you how to rigorously prove that 2+2=4 on Lean.
About the Author:
Ben Watkins finished his 4th year of mathematics at Cambridge in 2025. His interests include theoretical physics, quantum computation, and mathematical communication: sharing the joy of maths with a wider audience!
This content forms part of our collaboration with the Isaac Newton Institute for Mathematical Sciences (INI) – you can find all the content from the collaboration here.
The INI is an international research centre and our neighbour here on the University of Cambridge's maths campus. It attracts leading mathematical scientists from all over the world, and is open to all. Visit www.newton.ac.uk to find out more.
