"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, New York Times bestselling author of Infinite Powers , and co-host of The Joy of Why podcast "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." --Brian Christian, author of The Alignment Problem "[ THE PROOF IN THE CODE ] is science writing at its best: technically precise, conceptually ambitious, and consistently accessible. A rare achievement." --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 "This weird and wonderful book . 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 "[ THE PROOF IN THE CODE ] is 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 " 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.