Sometimes, a book perfectly meets its moment.
Publishing can be funny—it takes years to research, write, and edit a story, and the world it publishes into often looks quite different from when it was first signed up. In 2020, Kevin Hartnett reported on the IMO Grand Challenge, an early effort using a then-obscure program called Lean to train AI to compete in the International Math Olympiad. In the years since, we’ve seen a veritable explosion in machine-assisted mathematics. At the end of May 2026, an OpenAI model disproved Erdős’s famously tricky unit distance problem, which had remained unsolved for 80 years. The Leiden Declaration, published two weeks later, and now with over 2,000 signatories, acted as a state of the union on how mathematicians are thinking about AI.
It was into this upheaval that Kevin’s book THE PROOF IN THE CODE was released into the world. Suddenly (and happily!) everyone wanted to talk about math, computers, and AI. Kevin appeared on The New York Times tech podcast Hard Fork to discuss the Leiden Declaration, on The Quanta Podcast to outline the drastic shift from chalkboard to computerized mathematics, and on the Breaking Math Podcast to talk about his work on the book, the explosion of Lean into the mainstream, and the “perfect confluence between Lean and our current AI moment.”
Breaking Math co-host Noah Giansiracusa called it “the best math book I’ve read in years—the closest thing to capturing the magic of James Gleick’s Chaos. A true mathematical thriller!” (Order THE PROOF IN THE CODE here.)
In the midst of these virtual conversations, Kevin appeared with publisher Thomas Lin for a public conversation at the Simons Foundation, “Building a Truth Machine.” To a packed house, Kevin shared anecdotes from his years following Lean’s development and the conversations he’d had with the key figures shaping math and AI today. The two topics, he noted, are now inextricably linked:
“[Models] have gotten so much better because of reinforcement learning. And to do that, you need an environment to give a sharp feedback signal. [With] Lean, you can have the model basically do math problems, output the answers in Lean code, and get that instant feedback. … It’s why the big labs care… it’s just totally in the heart of the AI model training ecosystem.”
The two discussed the future of problem-solving in a world where AI—depending who you ask—could become anything from a mathematician’s helpful tool to their uncanny replacement. Kevin was hopeful about the future of human-computer collaboration, though he also offered this advice to students:
“You need to learn math. You need to learn it in the kind of way it’s always been learned, and understand the concepts, and wrestle with them. If you ever want to be someone like Terry Tao who’s directing AI, you need to have that deep level of understanding.” (You can watch the full video at the top of this post.)
Forthcoming Events
At the end of July, meet authors Kevin Hartnett and Terence Tao, and the Quanta Books team, at the International Congress of Mathematicians (ICM) in the Pennsylvania Convention Center in Philadelphia. The largest math conference in the world, ICM occurs once every four years, and this will be the first time it’s been held in the United States since 1986. Visit the Quanta Books Booth #102, where we’ll be selling copies of THE PROOF IN THE CODE and raffling away Quanta Books totes, T-shirts, and an early galley of Terence Tao’s SIX MATH ESSENTIALS.
Saturday, July 25, 11:00 AM to 12:00 PM
Bookplate Signing: Terence Tao
Location: Booth #102 (Hall E)
Terence Tao will sign bookplates for his forthcoming book, SIX MATH ESSENTIALS, which will be released on October 27 and is currently available for preorder. His simple yet elegant tour of six central math concepts—numbers, algebra, geometry, probability, analysis, and dynamics—“beautifully distills the essence of what math is…as only someone with his breadth of knowledge ever could,” in the words of 3Blue1Brown’s Grant Sanderson. And for our World Cup fans, math writer Ben Orlin raves that reading SIX MATH ESSENTIALS is “like seeing soccer through Messi’s eyes.”
Saturday, July 25, 1:15 PM to 2:15 PM
The Proof in the Code: A Conversation with Kevin Hartnett & Thomas Lin
Location: Benjamin Hall Stage (Hall E)
Kevin Hartnett will be in conversation with Thomas Lin about THE PROOF IN THE CODE. Afterward, he will sign copies of his book at the Quanta Books booth (#102).
You can register for ICM on the official website, or register for free public Math Festival events such as Kevin’s book event on Saturday, July 25, and Terence Tao’s ICM public lecture on Friday, July 24.
Hope to see you there!