Brian Christian, author of The Alignment Problem
“At a time when knowledge work is on the brink of a seismic transformation, math . . . offers us a vision of what may be coming. [Hartnett’s writing is] gripping, page-turning, lucid, and significant.”
The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett traces the development of Lean, a software system designed to verify mathematical proofs, and the community of researchers who adopted it.
Beginning with its origins at Microsoft Research, the book follows Lean’s evolution from a specialized programming tool into software used in mathematical research and artificial intelligence. Hartnett also introduces the mathematicians and computer scientists whose work helped shape the project and its adoption across different research communities.
Hartnett explores how formal proof systems are used to write, verify, and share mathematical proofs, using Lean as the central narrative. He discusses how these tools have influenced collaboration among mathematicians working on increasingly difficult problems.
The book also considers the role of formal proof systems in artificial intelligence research. Companies including Google DeepMind and Meta have explored these tools as part of their work on machine reasoning, prompting discussion about how computers may contribute to mathematical research.
Through the history of Lean and the people involved in its development, The Proof in the Code explores how formal verification is influencing research in mathematics and artificial intelligence.
The National CIO Review® is a proud supporter of Bookshop.org which connects readers with independent booksellers all over the world. We believe local bookstores are essential community hubs that foster culture, curiosity, and a love of reading, and we’re committed to helping them thrive. Every purchase at Bookshop.org financially supports independent bookstores.
