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
0 Comments