Book Notice: The Proof in the Code (2026)

Hartnett, Kevin. 2026. The Proof in the Code. Quanta Books.

Kevin Hartnett 2026 traces the development of the interactive theorem prover (ITP) Lean 4, developed by the Microsoft programmer Leonard De Moura, from the very first days in 2013 until the present day. As of today, Lean 4 is the most influential ITP in mathematics, being used by mathematicians such as Terry Tao on formalization projects. It is accompanied by a vast library of proofs and definitions called Mathlib. I enjoy reading biographical books, so I appreciated how Hartnett often added biographical material on the main characters in the story. 

Lean 4 is being used by more and more mathematicians and it is also being used by AI research units like DeepMind in the quest to develop AI theorem provers. Recently, a theorem prover (AlphaProof) received a silver medal in the International Math Olympiad. 

I especially enjoyed reading about the tension between De Moura and the mathematicians. De Moura was always leaning toward carefulness in the development of Lean 1, 2, 3, 4, whereas the mathematicians were pushing full speed ahead trying to get it to formalize as much mathematics as possible. I thought that the author could have put a bit more actual mathematics in the exposition, maybe adding it in appendices or in side boxes.

The book did a good job at describing Terry Tao’s open attitude toward the use of ITPs and AI in mathematics. It made me think of all the various ways in which computers could be used to aid in the development of formal syntax. I am not talking about LLMs, and whether or not they understand syntax, rather I am talking about using computational methods to study natural language syntax, as spoken and processed by human beings.

For example, at one point I was deeply involved in developing a program to process large amounts of cross-linguistic language data looking for cross-linguistic generalizations. But that was more than 15 years ago. With the explosion of AI and computational power, those efforts would take on a very different light nowadays.

Another angle might be formalization. Syntacticians have a long history of downplaying formalization, and of formulating vague hand-wavy arguments. I have argued many times in the past that formalization can help us to understand minimalist syntax better, and to help us make empirical predictions. Actually, developing a program (analogous to Lean 4) to support syntacticians doing formalization would be a genuine breakthrough in our field.