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 - 25 of 25 reviews
July 29, 2026
Anyone who has ever been deeply involved in an open source community will recognize the elements of this story: founding developers with partly conflicting and partly complementary goals, overtaxed maintainers, contributors who start off enthused and then fade away when the hard bits are needed, along with a few diehards who keep it running, worries about funding and academic vs industrial applications, etc. That said, Lean has been a meteorically successful project, growing from a single engineer's project to a small community to a fashionable framework, all the way to the foundation for many of the most legitimately impressive successes in software today, serving as the framework in which modern tools in AI for mathematics and code generation have been able to go from the unreliable curiosities they were 3 years ago to robust systems that can reliably solve simple coding tasks and contribute to solving open problems in math. Underneath it there are some intriguing ideas about the foundations of formal mathematics, which Hartnett, as a veteran math reporter, explains clearly but gently for a lay audience, and forays into the world of high level math, as Lean has started to play an important role in modern research mathematics.
I picked this up because, with AI code generation tools and forays of many research groups into automated formalization, textbook and even advanced research results in a variety of fields, including some touching on my own, have started to be translated into Lean, which looks likely to be an important part of bringing rigor to many mathematical research areas. Watching from the sidelines as a group of colleagues has been converting a textbook from which I used to teach a PhD level class has let me see both how much work this is; certainly not something achievable without AI assistance by people who are mathematically adept but not trained as mathematicians per se. But the fact that progress has been proceeding fairly smoothly in spite of that suggests that it will allow even those with a partial background to contribute rigorously. Hartnett's book is not a guide to actual use of Lean; there are code tutorials for that. But it has been useful context for what the program is all about and where it came from, and I recommend it to potential users in math-adjacent areas who might be on the fence.
I picked this up because, with AI code generation tools and forays of many research groups into automated formalization, textbook and even advanced research results in a variety of fields, including some touching on my own, have started to be translated into Lean, which looks likely to be an important part of bringing rigor to many mathematical research areas. Watching from the sidelines as a group of colleagues has been converting a textbook from which I used to teach a PhD level class has let me see both how much work this is; certainly not something achievable without AI assistance by people who are mathematically adept but not trained as mathematicians per se. But the fact that progress has been proceeding fairly smoothly in spite of that suggests that it will allow even those with a partial background to contribute rigorously. Hartnett's book is not a guide to actual use of Lean; there are code tutorials for that. But it has been useful context for what the program is all about and where it came from, and I recommend it to potential users in math-adjacent areas who might be on the fence.
Read
August 2, 2026fantastic narration of the creation and dramatis personae of the early years of Lean, the proof assistant programming language that's apparently become more mainstream in the Math community. Lean's usage and growth is honestly astounding as it's now also used in Alphaproof. This book is terrific as well, because it's hard to turn a story about abstruse math into something intensely captivating, or exciting for the general public, yet this book delivers in that sense
July 13, 2026
This was an informative microhistory of the Lean programming language which is finding uses in both the computer science/AI front and the math front. This is a good read for those in the software industry.
July 11, 2026
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.
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.
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.
August 3, 2026
Eine Geschichte der Programmiersprache Lean, die heutzutage viel von Mathematikern eingesetzt wird, um Beweise am Computer umzusetzen, anhand der Leute, die darauf Einfluss hatten. Ein Stern weniger, weil ich den Stil nicht mochte.
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.
July 1, 2026
The Proof in the Code is a captivating, remarkably accessible, and intellectually exhilarating account of one of the most significant developments in modern mathematics and artificial intelligence. Kevin Hartnett transforms what could have been a highly technical subject into a compelling human story about curiosity, collaboration, and humanity's enduring search for certainty.
One of the book's greatest achievements is its ability to explain the revolutionary significance of Lean without requiring readers to be mathematicians or computer scientists. Hartnett skillfully reveals how a relatively obscure proof assistant evolved from a specialized research tool into a technology reshaping mathematical discovery and influencing some of the world's leading AI laboratories. Complex concepts are introduced with clarity, making readers feel included in an unfolding scientific revolution rather than overwhelmed by it.
Equally compelling are the people behind the technology. Rather than focusing solely on software, Hartnett tells the stories of visionary individuals whose passion, persistence, and unconventional thinking transformed Lean into a movement. Figures such as Leo de Moura, Terence Tao, and Peter Scholze emerge not merely as brilliant researchers but as collaborators redefining how mathematics itself can be practiced in the twenty-first century.
The exploration of truth, proof, and certainty gives the book remarkable philosophical depth. Far beyond a history of software development, The Proof in the Code asks profound questions about how knowledge is established, how humans and machines can reason together, and what the future of intellectual discovery may look like as artificial intelligence becomes an increasingly capable partner rather than simply a computational tool.
Hartnett's journalistic style deserves particular praise. His writing combines technical precision with engaging storytelling, balancing historical context, personal narratives, scientific breakthroughs, and forward-looking analysis in a way that keeps readers fully invested throughout.
Perhaps most inspiring is the optimistic vision of human-computer collaboration that emerges. Rather than portraying AI as a replacement for human creativity, the book illustrates how tools like Lean amplify human reasoning, opening entirely new possibilities for mathematics, scientific discovery, and technological innovation.
The Proof in the Code is an outstanding work of science writing that successfully bridges mathematics, computer science, philosophy, and artificial intelligence. It offers readers an illuminating glimpse into a transformative moment in intellectual history and will appeal to mathematicians, programmers, AI researchers, technology enthusiasts, and anyone fascinated by the evolving relationship between human intelligence and machines.
One of the book's greatest achievements is its ability to explain the revolutionary significance of Lean without requiring readers to be mathematicians or computer scientists. Hartnett skillfully reveals how a relatively obscure proof assistant evolved from a specialized research tool into a technology reshaping mathematical discovery and influencing some of the world's leading AI laboratories. Complex concepts are introduced with clarity, making readers feel included in an unfolding scientific revolution rather than overwhelmed by it.
Equally compelling are the people behind the technology. Rather than focusing solely on software, Hartnett tells the stories of visionary individuals whose passion, persistence, and unconventional thinking transformed Lean into a movement. Figures such as Leo de Moura, Terence Tao, and Peter Scholze emerge not merely as brilliant researchers but as collaborators redefining how mathematics itself can be practiced in the twenty-first century.
The exploration of truth, proof, and certainty gives the book remarkable philosophical depth. Far beyond a history of software development, The Proof in the Code asks profound questions about how knowledge is established, how humans and machines can reason together, and what the future of intellectual discovery may look like as artificial intelligence becomes an increasingly capable partner rather than simply a computational tool.
Hartnett's journalistic style deserves particular praise. His writing combines technical precision with engaging storytelling, balancing historical context, personal narratives, scientific breakthroughs, and forward-looking analysis in a way that keeps readers fully invested throughout.
Perhaps most inspiring is the optimistic vision of human-computer collaboration that emerges. Rather than portraying AI as a replacement for human creativity, the book illustrates how tools like Lean amplify human reasoning, opening entirely new possibilities for mathematics, scientific discovery, and technological innovation.
The Proof in the Code is an outstanding work of science writing that successfully bridges mathematics, computer science, philosophy, and artificial intelligence. It offers readers an illuminating glimpse into a transformative moment in intellectual history and will appeal to mathematicians, programmers, AI researchers, technology enthusiasts, and anyone fascinated by the evolving relationship between human intelligence and machines.
August 1, 2026
Kevin Hartnett, that prolific writer for Quanta Magazine, has written the first book published by Quanta Books. It's a solid human-oriented history of Lean and its increasing importance in formalizing mathematics and in connection with AI.
I'm excited for the next two books coming out from Quanta: Six Math Essentials from Terry Tao, and Everything Is Fields from David Tong. In the latter case, it seems we have the Simons Foundation publisher publishing a book from a professor whose position is funded by the Simons Foundation. I did a Simons Foundation fellowship myself, but I mean... doesn't it seem like it would be great for things like this to not depend on hedge fund money? Regardless, those two books look like they should be great!
I hadn't realized how much Lean and even more so Z3 and other parts of de Moura's work are related to satisfiability. It's not exactly the same, but it's related even to the CP-SAT kinds of stuff I did a little bit of work with a while ago. (CP-SAT is Constraint Programming - Satisfiability, like OR-Tools. SMT is Satisfiability Modulo Theories, like Z3. And then Lean is basically a type checker with a lot of tooling for writing types: applied Curry-Howard correspondence.)
I tried the current version of the Natural Number Game and proved 2+2=4 using simple tactics. I installed Lean (doing it inside VSCode is highly recommended) but really the web version is enough to play around with.
It's a little strange reading a "history" that's so recent. Some of the more distant history was also interesting. I hadn't realized that Leibniz had an effort to formalize all human reasoning, and thought that people could settle disputes by using his system of formal logic. Hartnett failed to note that this was published when Leibniz was 20, and Leibniz seems to have later found it embarassing.
It's interesting thinking about the extreme formalization here in comparison to Cheng's book... The concern here is with correctness, like Bourbaki on steroids. Tao is excited about it because it helps math "scale" beyond what one person can do, what one person can understand, I think. If AI can write a proof, it can be verified formally, whether or not anyone understands how the proof works. It's almost the opposite mathematical view to what Cheng and I think is important, which is the human understanding aspect.
I'm excited for the next two books coming out from Quanta: Six Math Essentials from Terry Tao, and Everything Is Fields from David Tong. In the latter case, it seems we have the Simons Foundation publisher publishing a book from a professor whose position is funded by the Simons Foundation. I did a Simons Foundation fellowship myself, but I mean... doesn't it seem like it would be great for things like this to not depend on hedge fund money? Regardless, those two books look like they should be great!
I hadn't realized how much Lean and even more so Z3 and other parts of de Moura's work are related to satisfiability. It's not exactly the same, but it's related even to the CP-SAT kinds of stuff I did a little bit of work with a while ago. (CP-SAT is Constraint Programming - Satisfiability, like OR-Tools. SMT is Satisfiability Modulo Theories, like Z3. And then Lean is basically a type checker with a lot of tooling for writing types: applied Curry-Howard correspondence.)
I tried the current version of the Natural Number Game and proved 2+2=4 using simple tactics. I installed Lean (doing it inside VSCode is highly recommended) but really the web version is enough to play around with.
It's a little strange reading a "history" that's so recent. Some of the more distant history was also interesting. I hadn't realized that Leibniz had an effort to formalize all human reasoning, and thought that people could settle disputes by using his system of formal logic. Hartnett failed to note that this was published when Leibniz was 20, and Leibniz seems to have later found it embarassing.
It's interesting thinking about the extreme formalization here in comparison to Cheng's book... The concern here is with correctness, like Bourbaki on steroids. Tao is excited about it because it helps math "scale" beyond what one person can do, what one person can understand, I think. If AI can write a proof, it can be verified formally, whether or not anyone understands how the proof works. It's almost the opposite mathematical view to what Cheng and I think is important, which is the human understanding aspect.
June 25, 2026
This is a great little story about a very recent development in the history of technology and mathematics: the Lean software used for formalizing math proofs as computer code. The tool seems to mark a significant shift in the way mathematics can be done, and the book covers it's unusual emergence, the serendipitous conditions that lead to it's success, and its impact on the thoughts and lives of those involved.
Like most engaging histories, it's a story told about these individuals: their backgrounds, motivations, quirks, trials, and triumphs. As a mere math enthusiast (non-practising except where professional duty demands) I was easily able to follow the many technical twists, setbacks and achievements without feeling like it was being too dumbed-down.
While the concept/philosophy of "open source" software isn't really a theme explored much in the book, this is really a great oral history of an open source success story... of a community consisting mostly of volunteers working together (for the most part) on something they believed in as having intrinsic value, beyond financial or professional gain.
There are some celebrity names and companies popping up, particularly in the later parts - Terrance Tao, Google Deep Mind, which connected the dots on disparate tech news stories I'd seen over the years about Lean and AI and maths.
If, like me, you've developed a bit of a love/hate relationship with AI, and are wondering what you're in for ... the last third or so of the story gets entangled with modern generative AI, but the focus is mostly on the tech/math nerdery and the story mostly steers clear of broader ethical issues in the tech sector and the swirling culture wars that dominate the mid-2020s.
If you like stories of ambitious geeks on quixotic quests in the world of math and computer science, give this book a try.
FWIW I listened to the audiobook and couldn't see any formulae or illustrations but didn't feel like the telling suffered from it.
Like most engaging histories, it's a story told about these individuals: their backgrounds, motivations, quirks, trials, and triumphs. As a mere math enthusiast (non-practising except where professional duty demands) I was easily able to follow the many technical twists, setbacks and achievements without feeling like it was being too dumbed-down.
While the concept/philosophy of "open source" software isn't really a theme explored much in the book, this is really a great oral history of an open source success story... of a community consisting mostly of volunteers working together (for the most part) on something they believed in as having intrinsic value, beyond financial or professional gain.
There are some celebrity names and companies popping up, particularly in the later parts - Terrance Tao, Google Deep Mind, which connected the dots on disparate tech news stories I'd seen over the years about Lean and AI and maths.
If, like me, you've developed a bit of a love/hate relationship with AI, and are wondering what you're in for ... the last third or so of the story gets entangled with modern generative AI, but the focus is mostly on the tech/math nerdery and the story mostly steers clear of broader ethical issues in the tech sector and the swirling culture wars that dominate the mid-2020s.
If you like stories of ambitious geeks on quixotic quests in the world of math and computer science, give this book a try.
FWIW I listened to the audiobook and couldn't see any formulae or illustrations but didn't feel like the telling suffered from it.
August 4, 2026
The author chronicles the development of the Lean interactive theory prover and its relevance to AI mathematics. By using a formal Lean statement of a theorem as the input prompt, and requiring the LLM to output a Lean proof of it, we can be confident that the proof is correct. The proof could be very long and require human verification in the absence of using a formal language. But by using a formal language like Lean, we can use the Lean proof checker to verify it. Mathematics is in this sense easier for AI to handle than other subjects precisely because it is verifiable, given the use of a suitable formal language. If software engineers learned Lean and used it to write formal specifications then AI generated software would also be verifiable. This was in fact the original reason that Microsoft funded the development of Lean.
The author also discusses the personalities and politics behind Lean. It closely matches the events portrayed over the last decade in numerous YouTube videos by key actors including Leo de Moura, Kevin Buzzard, Jeremy Avigad, and Terrence Tao. However, he goes deeper on some key issues such as the tension between the needs mathematicians versus siftware engineers, and the foundational debate between simple type theory and dependent type theory.
My only criticism is that the mathematical discussion is a little too cursory, presumably because the author wants the book to be accessible to a broader audience. However, the whole topic is somewhat esoteric and unlikely to be of interest to readers with no or little background in mathematics or software engineering.
The author also discusses the personalities and politics behind Lean. It closely matches the events portrayed over the last decade in numerous YouTube videos by key actors including Leo de Moura, Kevin Buzzard, Jeremy Avigad, and Terrence Tao. However, he goes deeper on some key issues such as the tension between the needs mathematicians versus siftware engineers, and the foundational debate between simple type theory and dependent type theory.
My only criticism is that the mathematical discussion is a little too cursory, presumably because the author wants the book to be accessible to a broader audience. However, the whole topic is somewhat esoteric and unlikely to be of interest to readers with no or little background in mathematics or software engineering.
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 25, 2026
This is a solid history of Lean and how it's contributing to math formalization. I'm vaguely familiar with the area—I haven't used theorem provers much, but I've worked in adjacent areas in programming languages—so I found The Proof in the Code both accessible and interesting. It certainly filled in some gaps I had about how Lean evolved over time and, especially, how it expanded from formal verification and type theory into workaday mathematics.
I particularly liked how the book covered the social aspects of formalizing math. I've always thought that open source programming is a legitimately special social movement that is legitimately unique in an understated way; the fact that we can apply open source ideas, tools and practices to math is a major advance.
My only caveat is that the book might be a too high level for people who are not at least somewhat familiar with theorem provers or, at least, high-level programming and math. I suspect I filled in a lot of details based on my own experience without consciously realizing it, and the book will not convey the right mindset to people who don't already have some intuition for the field.
I particularly liked how the book covered the social aspects of formalizing math. I've always thought that open source programming is a legitimately special social movement that is legitimately unique in an understated way; the fact that we can apply open source ideas, tools and practices to math is a major advance.
My only caveat is that the book might be a too high level for people who are not at least somewhat familiar with theorem provers or, at least, high-level programming and math. I suspect I filled in a lot of details based on my own experience without consciously realizing it, and the book will not convey the right mindset to people who don't already have some intuition for the field.
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).
August 2, 2026
Very well written - anyone can read it, you don't need a math or computing background.
I knew some of the stories in this book from Hartnett's Quanta Magazine articles, but having the whole saga in one place made it easier for me to appreciate and understand.
If you're interested in how a non-hallucinatory AI might be built, this book will give you insight into how hard that really is, even in an area like math where the "true answer" to a question might seem clearcut.
It's also a fine human interest story. Hartnett brings the mathematicians and computer scientists in this saga alive. It ain't all sweetness and light - he brings out the stresses and quirks these people had. Find out how the unaffordability of housing in the SF Bay area changed the lives of some key players.
I knew some of the stories in this book from Hartnett's Quanta Magazine articles, but having the whole saga in one place made it easier for me to appreciate and understand.
If you're interested in how a non-hallucinatory AI might be built, this book will give you insight into how hard that really is, even in an area like math where the "true answer" to a question might seem clearcut.
It's also a fine human interest story. Hartnett brings the mathematicians and computer scientists in this saga alive. It ain't all sweetness and light - he brings out the stresses and quirks these people had. Find out how the unaffordability of housing in the SF Bay area changed the lives of some key players.
July 24, 2026
I wasn't sure if I would like this book, I am not a math or computer expert. I really enjoyed it and thought Hartnett did a great job building drama and making the subject matter understandable. Very timely book will help you understand the intersection of math, computer science, and AI with the personalities behind the innovations in these fields.
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 - 25 of 25 reviews