Book Review: The Proof in the Code
In just a few years artificial intelligence tools have progressed from solving formulaic math contest problems to generating novel proofs of long-standing open conjectures. The way math is done is changing, and more change is coming. Anyone interested in math should be paying attention to the unfolding story of AI-assisted mathematics, and this is especially true for math teachers, whose current students will enter a world where “doing math” is likely to mean something dramatically different than it does today.
Kevin Hartnett’s “The Proof in the Code” is an excellent entry point into that world. Hartnett tells the origin story of Lean, a mathematical formalization tool playing part in the AI-assisted mathematics revolution. Originally developed by researchers at Microsoft to debug code, Lean is now being used in synthesis with generative AI tools like large language models to debug mathematical proofs. The results have been astonishing.
“The Proof in the Code” is the story of the people and the ideas behind Lean, but it’s also the story about how we’ve arrived at a place where one of the world’s leading mathematicians recently felt obligated to say “It’s not necessarily the end of mathematics”. Hartnett’s book is a satisfying read for anyone interested in science and technology, but for teachers and learners of math, “The Proof in the Code” isn’t just a compelling tale of recent theoretical advances. It’s part of the backstory of the next chapter of human mathematics.
Related Posts
1 Comment
ShortCalc · October 4, 2026 at 2:52 pm
Thanks for this review — I hadn’t heard of Hartnett’s book, and the origin story of Lean sounds fascinating. The observation that AI tools have moved from solving formulaic contest problems to engaging with formal proof systems really captures how fast this space is changing. I’m curious how you see tools like Lean fitting into the classroom — as a way to teach rigorous reasoning, or more as a research aid? Either way, this is now on my reading list.