What do you think?
Rate this book
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
Not yet published
Expected 9 Jun 26The inside story of Lean, a computer program that answers the age-old How do you know if something is true?
It began as an obscure bug-checking program at Microsoft Research developed by a lone computer engineer named Leo de Moura. Then an unlikely crew of mathematical misfits caught wind of it and began to adopt it with messianic zeal. Their goal was to create a truth machine that could provide the rarest of all commodities in a complete, 100 percent guarantee that something is true. Its Lean.
As the movement grew and strengthened the program’s capabilities, it drew in two of the world’s most prominent Peter Scholze and Terence Tao. Google DeepMind, Meta AI, and other tech firms started using the program to supercharge computer reasoning. Now it’s remaking the multi-thousand-year history of how mathematicians work, collaborate, and assess truth, while charting a new path in the march toward machine intelligence.
In The Proof in the Code, Kevin Hartnett tells the definitive story of the birth and rise of Lean, and how a growing movement is transforming the enterprise of mathematics and ushering in a new era of human–computer collaboration. An engrossing, character driven narrative filled with insights about the future of math, computers, and AI, this brilliant work of journalism from one of the world’s leading math writers offers a profound answer to the Can computers reveal universal truths?
It began as an obscure bug-checking program at Microsoft Research developed by a lone computer engineer named Leo de Moura. Then an unlikely crew of mathematical misfits caught wind of it and began to adopt it with messianic zeal. Their goal was to create a truth machine that could provide the rarest of all commodities in a complete, 100 percent guarantee that something is true. Its Lean.
As the movement grew and strengthened the program’s capabilities, it drew in two of the world’s most prominent Peter Scholze and Terence Tao. Google DeepMind, Meta AI, and other tech firms started using the program to supercharge computer reasoning. Now it’s remaking the multi-thousand-year history of how mathematicians work, collaborate, and assess truth, while charting a new path in the march toward machine intelligence.
In The Proof in the Code, Kevin Hartnett tells the definitive story of the birth and rise of Lean, and how a growing movement is transforming the enterprise of mathematics and ushering in a new era of human–computer collaboration. An engrossing, character driven narrative filled with insights about the future of math, computers, and AI, this brilliant work of journalism from one of the world’s leading math writers offers a profound answer to the Can computers reveal universal truths?
288 pages, Hardcover
Expected publication June 9, 2026
3 people are currently reading
36 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 of 1 review
December 4, 2025
A brilliant history of mathematics (and computer science) book.
You can safetly gift it to anyone with a scientific graduate education. They will be delighted.
Here is what makes The Proof in the Code special:
* the writing is impeccable. Kevin Hartnett is easy to read, engaging, and does not go into unnecessary tangents. We follow the recent story of interactive theorem provers as if it were a thriller. The author introduces just the right amount of trivia and detail to keep us focused.
* everything is put into perspective, which makes it easier to understand the research and academic context surrounding the creation of Lean. A software tool is supposed to reduce friction for its users. Kevin Hartnett explains exactly which problems the authors were trying to solve, and why Lean ended up being a hit among mathematicians. It was not the first interactive theorem prover - Coq was the star before Lean took off. The book explains why this shift happened. The Coq toolchain was not easy to use for people who did not come from computer science. Lean bridged the gap.
* Kevin Hartnett makes the main stakeholders in this revolution relatable. They are not only reduced to their work in the world of math and computer science. We learn just enough about their private lives to get an idea of their personality. It makes the rest of the story easier to follow. I also think that personality plays a major role in scientific shifts. The Lean core team had very complimentary personalities and skillsets, which helped the project take off.
* The book slowly leads us to the next step of the revolution: Using formal methods to create an AI mathematician that can work on new proofs. One of the main issues of generative AI is reliability. Models trained on spitting out the most likely word are terrible at math, and if you tried to make ChatGPT count, you probably had a good laugh. Formal methods can be leveraged to close the gap, and Kevin Hartnett will explain you how and why (without going too much into the details of reinforcement learning).
* One last thing, sadly a negative one. This will be very hard to read for someone who has no idea about university level mathematics and computer science. You need to know what a mathematical proof *is* in order to feel engaged. You need to have some idea of how academia works. You need to know a little bit about functional programming and solvers (software designed to find optimal solutions, run simulations, and solve mathematical problems). Otherwise, it will be hard to grasp exactly what Lean does, and why it is important for mathematical research.
Thank you NetGalley and Farrar, Straus and Giroux for sending me an early version of this book for review. I feel extremely grateful and had a great time reading it.
Thank you Kevin Hartnett for your extremely well-documented work, engaging writing, and general enthusiasm about math. This is peak scientific journalism.
You can safetly gift it to anyone with a scientific graduate education. They will be delighted.
Here is what makes The Proof in the Code special:
* the writing is impeccable. Kevin Hartnett is easy to read, engaging, and does not go into unnecessary tangents. We follow the recent story of interactive theorem provers as if it were a thriller. The author introduces just the right amount of trivia and detail to keep us focused.
* everything is put into perspective, which makes it easier to understand the research and academic context surrounding the creation of Lean. A software tool is supposed to reduce friction for its users. Kevin Hartnett explains exactly which problems the authors were trying to solve, and why Lean ended up being a hit among mathematicians. It was not the first interactive theorem prover - Coq was the star before Lean took off. The book explains why this shift happened. The Coq toolchain was not easy to use for people who did not come from computer science. Lean bridged the gap.
* Kevin Hartnett makes the main stakeholders in this revolution relatable. They are not only reduced to their work in the world of math and computer science. We learn just enough about their private lives to get an idea of their personality. It makes the rest of the story easier to follow. I also think that personality plays a major role in scientific shifts. The Lean core team had very complimentary personalities and skillsets, which helped the project take off.
* The book slowly leads us to the next step of the revolution: Using formal methods to create an AI mathematician that can work on new proofs. One of the main issues of generative AI is reliability. Models trained on spitting out the most likely word are terrible at math, and if you tried to make ChatGPT count, you probably had a good laugh. Formal methods can be leveraged to close the gap, and Kevin Hartnett will explain you how and why (without going too much into the details of reinforcement learning).
* One last thing, sadly a negative one. This will be very hard to read for someone who has no idea about university level mathematics and computer science. You need to know what a mathematical proof *is* in order to feel engaged. You need to have some idea of how academia works. You need to know a little bit about functional programming and solvers (software designed to find optimal solutions, run simulations, and solve mathematical problems). Otherwise, it will be hard to grasp exactly what Lean does, and why it is important for mathematical research.
Thank you NetGalley and Farrar, Straus and Giroux for sending me an early version of this book for review. I feel extremely grateful and had a great time reading it.
Thank you Kevin Hartnett for your extremely well-documented work, engaging writing, and general enthusiasm about math. This is peak scientific journalism.
Displaying 1 of 1 review