In The Proof in the Code, the journalist chronicles how the Lean programming language is fundamentally changing mathematics research and transforming AI.

What is Lean?

Lean is a special type of computer program that uses the rules of logic to tell you when something is true or not. It was designed starting in 2013 by Leo de Moura, a computer scientist at Microsoft Research who wanted Lean to be used for verifying the truth of software programs—does the software do exactly what it’s supposed to do without bugs? But soon after, a small group of enthusiastic mathematicians recognized that Lean could be used for verifying a different kind of truth, mathematical truth, which Lean does by checking whether all the logical steps in a proof are correct.

Is Lean an extension of AI or a tool to enable AI to become more powerful?

This was one of the great surprises of the book. When I started writing two years ago, Lean and AI had nothing to do with each other. Now, they’re deeply intertwined. AI, by which I mean large language models, makes Lean more powerful because it can search for potential proofs that Lean can check. Even more importantly, Lean can be used to train AI, through the process of reinforcement learning, and can be a safeguard for checking that computer code produced by LLMs works and isn’t riddled with errors or security flaws.

Is Lean close to being able to make mathematical discoveries rather than just checking the validity of proofs proposed by mathematicians?

It’s happening already. There are several highly funded, highly valued startups like Math Inc., Harmonic, and Axiom that are combining AI and Lean to solve open math problems. So
far, none of these results are shaking the field. But the trendline toward increasingly big discoveries is clear.

What’s your biggest challenge translating highly abstract ideas into prose accessible to general readers?

I’m not a mathematician, so I’m learning this material alongside my readers. The hardest part is forming my own correct conceptual understanding of what’s going on. That can take weeks in some cases, and it’s always a struggle. But once the pieces fall together in my head at the right level of detail, it feels relatively straightforward to communicate that to readers.

Your book is about people as much as it is about a computer program.

The Proof in the Code is about lots of big ideas, but it’s also fundamentally a character-driven book. You meet de Moura, the dogged auteur behind Lean; Jeremy Avigad, a top-notch academic who has a CEO-like ability to build alliances; and Kevin Buzzard, the uncensored showman who becomes Lean’s most prominent proselytizer. What I enjoyed most about writing the book was immersing myself in their stories.