Quanta Books Releases The Proof in the Code

One of the largest shifts in the history of mathematics is happening right now, and a new book from Quanta Books chronicles the people and project responsible. At the heart of this revolution is Lean, a programming language and proof assistant that serves as a “truth machine,” guaranteeing that a given proof is 100 percent correct.

The book’s author, Kevin Hartnett, first began reporting on Lean six years ago in a piece for Quanta Magazine (an editorially independent publication of the Simons Foundation). In the years since, he’s witnessed how Lean has changed the field. “It was arguably the biggest shift in how mathematicians worked in the multimillennia history of the subject,” he says.

Hartnett’s book, The Proof in the Code, is out today. An excerpt from the book on mathematician Terence Tao’s rise as a prominent voice in support of the potential of machine-assisted mathematics is now available on Quanta Magazine.

The book tells the stories of Lean’s developers and evangelists. It highlights Lean’s creator, Leo de Moura, a computer scientist who initially developed Lean at Microsoft Research and has championed its growth for over a decade. It also follows the project’s biggest proponents — Jeremy Avigad, Kevin Buzzard, Johan Commelin and Patrick Massot — who embraced the tool and spread the word about its potential.

“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,” Hartnett says.

The Proof in the Code is the first book from Quanta Books, a partnership imprint from the Simons Foundation and Farrar, Straus and Giroux. Quanta Books has a slate of exciting new releases on the horizon, with Terence Tao’s book Six Mathematical Essentials set for publication in October 2026.