I am a journalist covering math, computer science, and AI.
“A thrilling account … Readers will be captivated.”
Quanta Books / Farrar, Straus and Giroux
THE PROOF IN THE CODE
How a Truth Machine is Transforming Math and AI
The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true?
Coming June 2026
Pre-orderPraise for 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’ . . . . Readers will be captivated.”
-
“A fascinating example of how cultural clashes and creativity can create new paradigms . . . [In THE PROOF IN THE CODE] proofs, personalities, and machines collide—intriguingly—at the uneasy intersection of mathematics and computer science.”
-
“Kevin Hartnett is one of today’s finest chroniclers of math. With marvelous clarity and narrative flair, he introduces us to computer-verified proof, the drama behind it, and the people reimagining what math can be.”
-
“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.”
-
“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. Kevin Hartnett transforms work in a famously dense domain into a lucid and compelling narrative about how we decide what to trust, in both machines and ourselves. This is science writing at its best: technically precise, conceptually ambitious, and consistently accessible.”
-
“Lean is one of the most important things happening to math right now—future generations may come to regard it as the Euclid’s Elements of our time. In THE PROOF IN THE CODE, Kevin Hartnett perfectly captures the unlikely story of Lean’s birth and development.”
-
“I loved this weird and wonderful book! You don’t need to like math—or understand code—to grasp why this story matters. 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.”
-
“A narrative tour de force about the confluence of computer science, math and AI. Kevin Hartnett has the unique ability to tell stories about math and mathematicians, while seamlessly slipping in expositions of complex ideas. A must-read if you want to understand how machine-verifiable math is supercharging the next generation of AI.”
-
“THE PROOF IN THE CODE is about the people building a new way of creating mathematics, their ambitions, their uncertainties, their false starts and long leaps. Highly recommended.”
