What do you think?
Rate this book
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
The 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?
271 pages, Kindle Edition
Published June 9, 2026
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 13 of 13 reviews
June 14, 2026
An interesting history of Lean and it's importance to Math and AI
A really beautiful little book on the development of Lean and it's implications for Math and AI. The style is accessible but hits on some of the real underlying technical issues. A eye opening pleasure to rear.
A really beautiful little book on the development of Lean and it's implications for Math and AI. The style is accessible but hits on some of the real underlying technical issues. A eye opening pleasure to rear.
June 10, 2026
An extremely fascinating story. I went to Zulipchat and mastodon to read the old posts mentioned in the book.
I am not quite ditching Agda in favor of Lean yet, but as a book, amazing. A++.
I am not quite ditching Agda in favor of Lean yet, but as a book, amazing. A++.
June 12, 2026
This is, I’ll just say it, the most interesting book I’ve ever read about math. Much better than One Fish, Two Fish, Red Fish, Blue Fish which can get pretty boring, especially after a few dozens of rereads.
May 25, 2026
Does a great job of explaining advanced, theoretical level mathematics, how Lean software works and how it helped advance mathematics, and how that in turn was unfortunately used to power the current generative AI advances we're seeing. Eurgh.
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.
Review of advance copy received from Netgalley
This has been an intriguing book, a story that needed to be told.
It's all about how Lean was created as a tool for bugs and how it was transformed by mathematicians into their favorite program, up to the point of being instrumental for many AI projects.
The story is nicely written, easy to read and engaging. It's a tale that encompasses so much: great minds in pursuit of their passion, with fun and curiosity and a faith to bring a new tool to a whole domain, the camaraderie and community that builds around this, and the founder's struggle to maintain a project that took a life of its of its own.
The book also captures a very specific moment in time, that needed its own book: both for the field of math and also for computer science: the first time the mathematicians, in great number, switched to relying both on computers and towards a more collaborative view of their work. And for computer science the very small time frame when a tool pre-AI became part of it. And even when its founder and its funding suffered from the very emergence of AI.
Overall, this was a great read, a beautiful keepsake of these times before Ai and the passionate people who gave so much of their time and energy for their vision that benefits science and at large, the world.
It's all about how Lean was created as a tool for bugs and how it was transformed by mathematicians into their favorite program, up to the point of being instrumental for many AI projects.
The story is nicely written, easy to read and engaging. It's a tale that encompasses so much: great minds in pursuit of their passion, with fun and curiosity and a faith to bring a new tool to a whole domain, the camaraderie and community that builds around this, and the founder's struggle to maintain a project that took a life of its of its own.
The book also captures a very specific moment in time, that needed its own book: both for the field of math and also for computer science: the first time the mathematicians, in great number, switched to relying both on computers and towards a more collaborative view of their work. And for computer science the very small time frame when a tool pre-AI became part of it. And even when its founder and its funding suffered from the very emergence of AI.
Overall, this was a great read, a beautiful keepsake of these times before Ai and the passionate people who gave so much of their time and energy for their vision that benefits science and at large, the world.
Review of advance copy received from Netgalley
Kevin Hartnett’s The Proof in the Code covers one of the biggest shifts in mathematical history, the move from human intuition to computer-verified proof. It’s expertly researched and unexpectedly gripping.
The human stories are fascinating. Tom Hales spent years fighting to get peers to trust his computer-assisted proof. Kevin Buzzard had a full-on professional crisis that pulled him into the world of digital mathematics. These aren’t the kinds of stories you expect from a book about theorem provers, but they keep you engaged.
The arc is impressive. Hartnett connects a 1611 realization about snowflakes and a related puzzle about stacking oranges all the way to Google DeepMind and AlphaProof. The section on the breaking point in peer review for computer-assisted proofs is particularly well written. It gives the book a tension that carries you through the denser parts.
The book has a good amount of detail around Lean 2 vs. Lean 3, ITP libraries, and the cold-start problem. It’s top-tier science writing. If you want to understand where AI and mathematics are actually headed, it’s worthwhile reading.
The human stories are fascinating. Tom Hales spent years fighting to get peers to trust his computer-assisted proof. Kevin Buzzard had a full-on professional crisis that pulled him into the world of digital mathematics. These aren’t the kinds of stories you expect from a book about theorem provers, but they keep you engaged.
The arc is impressive. Hartnett connects a 1611 realization about snowflakes and a related puzzle about stacking oranges all the way to Google DeepMind and AlphaProof. The section on the breaking point in peer review for computer-assisted proofs is particularly well written. It gives the book a tension that carries you through the denser parts.
The book has a good amount of detail around Lean 2 vs. Lean 3, ITP libraries, and the cold-start problem. It’s top-tier science writing. If you want to understand where AI and mathematics are actually headed, it’s worthwhile reading.
June 11, 2026
Know what you are getting. This is touted as a Math and AI book. Yes, this sounds boring. However, this is not what you are getting. This book almost reads like a thriller. I don't know how the author did that. I have the audiobook.
I am not a mathematician. I am also not a typical coder. This book, based on the premise of Math programming and proof, should have been boring but I finished it in a 24 hour period. I didn't want to put it down and found myself excited about where the history was going and what the future had in store.
The author outlines the problem of getting mathematicians to use computer programs to help prove if a study was correct. There are several examples of experiments and hypothesis being proved as correct or being corrected when utilizing a tool, Lean, that was not originally designed for math but rather to help correct code and reduce errors in programming.
I am still baffled by how I found this book so entertaining. That says something about the quality of the writing and the narration.
Writing 5/5
Narration 5/5
Overall a surprising 5/5
I am not a mathematician. I am also not a typical coder. This book, based on the premise of Math programming and proof, should have been boring but I finished it in a 24 hour period. I didn't want to put it down and found myself excited about where the history was going and what the future had in store.
The author outlines the problem of getting mathematicians to use computer programs to help prove if a study was correct. There are several examples of experiments and hypothesis being proved as correct or being corrected when utilizing a tool, Lean, that was not originally designed for math but rather to help correct code and reduce errors in programming.
I am still baffled by how I found this book so entertaining. That says something about the quality of the writing and the narration.
Writing 5/5
Narration 5/5
Overall a surprising 5/5
Review of advance copy received from NetGalley
4.5 stars
Proof in the Code traces Lean’s development from inception through Lean 4 and its emergence as a key tool in the AI revolution. Kevin Shen’s narration made it easier to follow.
The dual lens is what makes it work: the personal side of open-source with the “many hands make light work” approach, plus the high-stakes of research institutions; alongside the story of how a proof-verification system became the target for building AI problem-solving engines. I especially liked the framing of invention as an uneven road — breakthroughs and plateaus, personality conflicts, not a clean arc. That said, the mathematical detours sometimes ran long and dragged the narrative.
Still, a great reminder that the modern AI revolution has been the work of many minds across many disciplines.
*Thanks to Macmillan Audio & NetGalley for the advance audio copy
Proof in the Code traces Lean’s development from inception through Lean 4 and its emergence as a key tool in the AI revolution. Kevin Shen’s narration made it easier to follow.
The dual lens is what makes it work: the personal side of open-source with the “many hands make light work” approach, plus the high-stakes of research institutions; alongside the story of how a proof-verification system became the target for building AI problem-solving engines. I especially liked the framing of invention as an uneven road — breakthroughs and plateaus, personality conflicts, not a clean arc. That said, the mathematical detours sometimes ran long and dragged the narrative.
Still, a great reminder that the modern AI revolution has been the work of many minds across many disciplines.
*Thanks to Macmillan Audio & NetGalley for the advance audio copy
June 10, 2026
I got the audiobook today, and finished it today. I found the story behind Lean very interesting, and enjoyed reading about all the interactions among all the computer scientists, mathematicians, and software engineers. Would someone who isn't involved in adjacent or directly related work find this book as fascinating? Hard to say, so maybe try the sample to see what you think. But I really appreciated getting this inside scoop on all these different personalities.
The author did an exhaustive investigation to piece all these components together. It sounded like he may even had access to private emails, although I'm not positive about that.
I hope the author does a postscript somewhere, or another book, on the recent developments with LLMs and mathematical problem solving (for example, the Open AI disproof of the Unit Distance Conjecture).
The author did an exhaustive investigation to piece all these components together. It sounded like he may even had access to private emails, although I'm not positive about that.
I hope the author does a postscript somewhere, or another book, on the recent developments with LLMs and mathematical problem solving (for example, the Open AI disproof of the Unit Distance Conjecture).
June 18, 2026
The Soul of a New Machine
I think this book is on the same level as Tracy Kidder's "The Soul of a New Machine." It really covers the human actors in the creation of a major technology.
I think this book is on the same level as Tracy Kidder's "The Soul of a New Machine." It really covers the human actors in the creation of a major technology.
June 20, 2026
It’s been a long time since I’ve had such a strong reaction to a book as I did reading The Proof in the Code! The way the narrator describes the story and the key points really grabbed my attention, and it makes you curious to see what happens next. I highly recommend it!
June 19, 2026
Really interesting exciting story of how open source projects get developed.
Displaying 1 - 13 of 13 reviews