“The Proof in the Code: How a Truth Machine Is Transforming Math and AI” by Kevin Hartnett

Main Index / Reviews Index / Nonfiction Reviews Index / 2026 Reviews Index

Rating: 5/5 Stars.

A fascinating book that looks at the field of computer aided mathematical and software proofs, and especially at Lean, currently the most talked about software used to analyse and show that mathematical proofs are correct and that software executes as designed.

The book starts with a mathematician who sets out to prove the Kepler conjecture about the packing of spheres in three dimensions. But the proof requires the use of computers to work through numerous packing methods. At the time, the use of computers to prove a conjecture was new, and mathematical journals were not keen to accept the proof as valid. From there, the book moves on to various attempts to create software that could be used to validate mathematical proofs. But the methods used were either too basic for advanced mathematical use, or the software was too complicated and made for the wrong target audience: they were created by computer scientists, not mathematicians, who had different requirement for what computers should do to validate a proof.

Then, Leonardo de Moura creates the program, Lean. In the process of creating Lean, he consults with mathematicians about what they want, as he is keen for his program to be used, not just as a research project. He also makes the code Open Source, and accepts outside contributions to make the code better. This gathers the attention of other mathematicians, including those keen to use computers to validate proofs.

Based on their requests, Lean is improved, and many mathematical concepts required as steps in proofs are encoded in Lean. But this puts pressure on de Moura, who wants to improve the core of Lean, not just keep adding mathematical concepts. Eventually, the mathematical concepts are split from the core of Lean and released as a separate library which the mathematicians maintain, leaving him free to work on Lean.

The Lean and the mathematical library becomes more capable, some mathematicians decide to get attention by coding the latest mathematical concepts and proof into Lean, to show that Lean was capable of showing that the latest proofs were valid. This gets the attention of top mathematicians like Terence Tao, who used Lean, liked what it is capable of, and advocate for its use.

In the present day, AI systems and Lean are now working in tandem to advance the field of mathematics. Mathematical concepts and proofs are generated by AIs, who then use Lean to provide feedback on whether the proof are correct or now. The feedback is then used to correct and generate more proofs. Mathematicians oversee the process to ensure that the proofs are of use and to add new ideas to the cycle for processing.

This is a book that gives a good up-to-date look at where the field of computer generated and validated proof stands. There are mathematicians who still do most of their thinking without computers, but even they benefit by ensuring that the final proof that they produce are shown to be valid by programs such as Lean.

Book read from 2026/07/07 to 2026/07/10.