Today we publish our first book, Kevin Hartnett’s THE PROOF IN THE CODE! Kevin’s singular account of the birth and rise of Lean reveals how a little-known programming language and proof assistant is ushering in the biggest modern shift in the way mathematicians seek truth—3Blue1Brown creator Grant Sanderson says “future generations may come to regard [Lean] as the Euclid’s Elements of our time.”
To mark the occasion, we asked Kevin to share a few words about why he was motivated to write this book:
“When I first reported about Lean and Mathlib for Quanta Magazine six years ago, it seemed like a quixotic quest.
“The idea of writing math proofs as computer code—so their correctness could be checked automatically—had been around for decades but had never caught on. Mathematicians didn’t really have trouble determining when a proof was right or not, and viewed “formal” computer mathematics as a lot of effort for minimal return.
Kevin unboxing his books at home. “Fast-forward to late 2023, when I started writing THE PROOF IN THE CODE. A lot had changed and it was clear there was a larger story there. Increasingly, the kind of digital, auto-verified results Lean made possible seemed like the future of mathematics. It was arguably the biggest shift in how mathematicians worked in the multi-millennia history of the subject.
“THE PROOF IN THE CODE focuses on the visionaries who made that transformation possible, including Leo de Moura, the driven computer scientist at Microsoft Research who created Lean and pursued his ambitions for the program over the course of more than a decade. The book also follows the stories of the eclectic crew of mathematicians—Jeremy Avigad, Kevin Buzzard, Johan Commelin, Patrick Massot—who, each for their own reasons, became Lean’s first adopters and most eager evangelists.
“My book comes out tomorrow, and even now the story is far from over. As I interviewed the main sources and read through the tens of thousands of messages they exchanged, the rapid rise of artificial intelligence was turbocharging Lean’s relevance. The world was about to be swamped with more AI-generated mathematics than human reviewers could possibly check—yet because of Lean, and its unerring ability to separate true results from false ones, they wouldn’t need to do it alone.
“Looking back on the story now, and Lean’s unlikely ascent to the prominent place it occupies in math today, two things strike me most. The first is the degree to which Lean’s adoption among mathematicians was the direct result of the efforts of the small band of people I chronicle in the book. Through sheer enthusiasm and doggedness, they shifted the field.
“The second is the absolutely perfect confluence between Lean and this present moment. I know that Leo can hardly believe how central the software program he created has become to the development of artificial intelligence—technology that was still science fiction when he started work on Lean in 2013. Sitting here today, recalling how much of a longshot Lean seemed when I first learned about it, I can hardly believe it either.”
Quanta Magazine ran an excerpt of the book yesterday, on how Terence Tao became “the most prominent public voice touting the potential of machine-assisted mathematics”:
“Terry Tao had found a new way of doing mathematics, and he showed no signs of going back.”
Order Kevin’s book here.
Mentions
Last Friday, Kevin appeared on The New York Times tech podcast Hard Fork to talk about big recent news in math and AI, including an OpenAI model’s disproof of one of the most important Erdős problems and the drafting of the Leiden Declaration. Host Kevin Roose proclaimed THE PROOF IN THE CODE “the most interesting book I’ve ever read about math.”
THE PROOF IN THE CODE was also mentioned in the Quanta Podcast episode “The AI Revolution in Math Has Arrived,” featuring math writer Konstantin Kakaes. While reviewing the current state of AI use in mathematics, host Samir Patel and Kakaes discuss the importance of formalizing mathematics—and the crucial role Lean is playing—in closing the gap between human language proofs and rigorous logic, and the importance of formalizing AI output in building trust in these ubiquitous models.
On LinkedIn, master math educator Patrick Honner called THE PROOF IN THE CODE “an excellent entry point into” the “unfolding story of AI-assisted mathematics.” The book, Honner says, “isn’t just a compelling tale of recent theoretical advances. It’s part of the backstory of the next chapter of human mathematics.”
In their June roundup of forthcoming titles, The Paris Review highlighted a fun excerpt from the book—a run of the mathematician Kevin Buzzard’s frenetic Gitter messages:
A starred Publishers Weekly review deemed THE PROOF IN THE CODE “a thrilling account of ‘how one man’s quest to build a truth machine—a computer program that can provide a complete, 100 percent guarantee that a chain of logic is correct—is transforming the field of mathematics.’”
And we’re thrilled to share early praise from fellow authors:
“Kevin Hartnett is one of today’s finest chroniclers of math. With marvelous clarity and narrative flair, he introduces us to … the people reimagining what math can be.” —Steven Strogatz, New York Times bestselling author of Infinite Powers and co-host of The Joy of Why podcast
“Remarkable. Kevin Hartnett’s writing about mathematics is as compulsively readable as any I’ve read. At a time when knowledge work is on the brink of a seismic transformation, mathematics itself offers us a vision of what may be coming to other fields—AI included. Gripping, page-turning, lucid, and significant.” —Brian Christian, author of The Alignment Problem
“THE PROOF IN THE CODE is a rare achievement: a deeply informed account of modern mathematics and computer science that is also genuinely exciting to read … This is science writing at its best: technically precise, conceptually ambitious, and consistently accessible.” —Seth Mnookin, author of The Panic Virus
“I loved this weird and wonderful book … THE PROOF IN THE CODE, written by the one person with the perspective to connect mathematicians, engineers, and the rise of AI, reveals why a technical idea hiding in plain sight could determine whether the machines we build will ever deserve our complete trust.” —Amy Webb, author of The Big Nine
“A narrative tour de force about the confluence of computer science, math and AI … A must-read if you want to understand how machine-verifiable math is supercharging the next generation of AI.” —Anil Ananthaswamy, author of Why Machines Learn and Through Two Doors at Once
A huge thanks to our readers who’ve supported our mission to publish serious, curiosity-driven nonfiction about serious math and science. We’re so excited for you all to read Kevin’s book!
