The Proof in the Code
By Kevin HartnettAbout the Book
THE PROOF IN THE CODE is the definitive account of the birth and rise of Lean, a proof assistant developed at Microsoft that is transforming the enterprise of mathematics and ushering in a new era of human-computer collaboration. Although Lean was originally conceived of as a code-checking program, a small group of mathematicians recognized its potential to become something far more powerful: the “truth oracle” that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex. This is the story of the grassroots effort to make that dream a reality. Filled with insights about the future of math, computers, and AI, THE PROOF IN THE CODE is a brilliant work of journalism by Kevin Hartnett, a leading math writer whose research and reporting offer a profound answer to a longstanding mystery: Can computers reveal universal truths?
Reviews
“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.” — Steven Strogatz, acclaimed Cornell mathematician, 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. 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.” — Seth Mnookin, author of The Panic Virus
“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.” — Grant Sanderson, creator of 3Blue1Brown
“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.” — Amy Webb, author of The Big Nine
“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.” — Anil Ananthaswamy, author of Why Machines Learn and Through Two Doors At Once
“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.” — Jordan Ellenberg, author of How Not to Be Wrong
About the Author
Kevin Hartnett is a math and technology writer whose work has been published widely in outlets including Quanta Magazine, The Atlantic, The Boston Globe, WIRED, Nautilus, and Scientific American. He was previously the senior writer at Quanta Magazine covering mathematics and computer science. His work has been collected in multiple volumes of the Best Writing on Mathematics series from Princeton University Press. From 2013 to 2016 he wrote “Brainiac,” a weekly column for The Boston Globe’s Ideas section. He lives in Yarmouth, Maine.