Euler's Eyes
2026-10-26
Notation for machines: proofs the computer checks
For two thousand years, a mathematical proof was a text written to be read by people. It could skip “obvious” steps, lean on a drawing, use the conventions of the community. The reader filled in the rest. In the last fifty years a reader has appeared that fills in nothing: the computer.
The four colours
How many colours are enough to colour any map so that neighbouring countries have different colours? The answer, four, was conjectured in 1852 and resisted for over a century. In 1976 Kenneth Appel and Wolfgang Haken, of the University of Illinois, proved it by reducing the problem to almost two thousand cases that a computer checked one by one, in more than a thousand hours of machine time.
The community was divided. Is a proof that no human being can read in full a proof? Its defenders recalled that many long proofs are not read in full by anyone either; its critics, that a program can have bugs. In 2005 the Frenchman Georges Gonthier wrote the whole proof, including the computer part, in a proof assistant called Coq, which checks each logical step from the axioms. The doubt moved: it was no longer “is the program right?” but “is the checker right?”, a much smaller program that is easier to audit.
The Kepler conjecture
In 1611 Kepler claimed that the densest way of stacking oranges is the greengrocer’s pyramid. In 1998 the American Thomas Hales announced a proof that combined hundreds of pages with extensive computer calculations. A team of referees worked for four years and declared itself “99% certain” of its correctness. Hales did not settle for the 1% and started the Flyspeck project to write the whole proof in a formal language. In 2014, with dozens of collaborators, the project was finished: the machine had checked every step.
Lean
The proof assistant most used by mathematicians today is Lean, created in 2013 by the Brazilian Leonardo de Moura, then at Microsoft Research. Around it grew mathlib, a collective library with hundreds of thousands of formalised theorems, written by hundreds of people. In 2020 the German Peter Scholze, a Fields medallist, challenged the community to formalise a result of his that he himself was not sure he had checked in every detail. The Liquid Tensor Experiment ended in 2022: the result was right, and the formalisation found simplifications in the proof.
A line of Lean looks like this:
theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b
“For any natural numbers $a$ and $b$, $a + b = b + a$, and the proof is the library’s commutativity theorem.” Nothing is left implicit: the type of each letter, the origin of each step. It is the linear writing of chapter 7 taken to the extreme, and the proof in words of chapter 4 translated into a grammar a machine can check.
Exercise: when three colours are not enough
A central country is surrounded by three countries, and each of those three borders the other two. Show that this map needs four colours.
The four countries border each other two by two: the central one touches all three, and the three touch each other. So each needs a colour different from all the others, and four are necessary. The theorem guarantees that five are never necessary, however complicated the map.
Exercise: read the line of Lean
In the line theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b, identify the hypothesis, the statement and the proof.
(a b : ℕ) declares the letters: $a$ and $b$ are natural numbers, like the “let $a$ and $b$ be natural numbers” of a text. After the colon comes the statement, $a + b = b + a$. After := comes the proof, which here is just a reference to a theorem already proved in the library. Algol’s :=, which we saw in text 5, reappears with a new meaning: “is defined as”, or “is proved by”.
Chapter index · ← Street mathematics and school mathematics: mathematics off the page · Notation and culture: a guide and a glossary →