The Mathematicians Who Bet Their Careers on a Microsoft Side Project

A decade ago, a small group of researchers walked away from the work they'd already built to chase an idea almost no one thought would matter. They were right.

Kevin Hartnett’s new book, “The Proof in the Code,” is out now from Quanta Books. We talked with him about all of it — Leo de Moura, Mathlib, the cold-start years, Peter Scholze, and what Lean means for a world where AI is generating math faster than anyone can read it.

🎧 Listen to the full conversation on YouTube

or Apple Podcasts.

Some math problems never makes it onto a chalkboard: the line you skip because everyone in the room already knows it’s true. Mathematicians do this constantly, and for good reason. A proof written out in full, with every assumption stated and every step justified, would be unreadable. So mathematicians compress and they write the headline steps and trust that any qualified reader can fill in the rest. It is an act of communication between people who already speak the language.

It is also a problem. Noah and I had the opportunity to dive into this a little deeper with Kevin Hartnett, author of “The Proof in the Code.”

In the early 2010s, a programmer at Microsoft Research named Leonardo de Moura was not trying to solve a problem in mathematics. He was trying to solve a problem in software: how do you guarantee that a program — something running inside Windows or Excel — does exactly what it’s supposed to do, and nothing else? The traditional approach is to test extensively and patch what breaks. De Moura wanted something stronger: a way to mathematically prove a program correct, the same way a geometry student proves two triangles congruent.

The tool he built to do this is called Lean. And the strange, decade-long detour it took — from a bug-catching utility with no real audience, to the thing a small band of mathematicians adopted as a new way of doing math, and then to a piece of infrastructure now sitting at the center of how artificial intelligence verifies its own work — is the subject of Hartnett’s book.

Hartnett has been reporting on Lean since 2020, when he wrote about the construction of Mathlib, a kind of communal library of formally defined mathematical concepts that any Lean user can draw on. He returned to the subject for a simple reason: by late 2023, it had become clear that Lean was not a passing experiment. It had, in his words, achieved escape velocity.

What makes the book work is that it resists the temptation to be a story about software; it is a story about people.

The four or five mathematicians at the center of the book had, by most measures, already succeeded. They had research careers, reputations, the kind of mid-career security that doesn’t get walked away from lightly. They did it anyway — not because Lean was finished or proven, but it offered a different way of being certain about something. For years, nobody knew if it would catch on. The book’s drama, such as it is, comes from watching a small number of true believers try to convince a skeptical field that formality was worth the enormous tedium it demanded.

That tedium is not incidental to the story; it is the story. A typical chalkboard proof, formalized fully in Lean’s language, can run twenty to a hundred times longer than the version a mathematician would write by hand — a ratio researchers call the de Bruijn factor. Writing math in Lean means specifying every single logical step, the way a computer program cannot skip a line and simply “know” what comes next. Hartnett’s analogy is the right one: a chalkboard proof is a sketch of an argument between people who trust each other. A Lean proof is the argument written out so completely that a machine with no judgment at all can check whether it holds.

This is, on its face, a deeply unglamorous trade. So why bother?

Because something has changed in the last two years, and it isn’t really about mathematicians anymore. It’s about what happens when the thing generating proofs is not a person at all.

Artificial intelligence is now capable of producing mathematical arguments — sometimes good ones — faster than any human community could read and check them by hand. Hartnett’s book ends right before this became fully apparent; in his telling, the story has already changed twice since he submitted the manuscript. The questions that used to be academic — can we trust this proof? did the maintainer make an error formalizing this definition? — have become urgent in a different way. If an AI system generates ten thousand candidate proofs, a human cannot read all of them. Something has to do the checking. Lean, or something functionally like it, is the leading candidate.

It’s worth being precise about what this buys you and what it doesn’t. Lean can guarantee that a piece of code does exactly what its formal specification says it does. It cannot tell you whether that specification captures what you actually meant — the same gap that produces the AI alignment nightmares people worry about, where a system satisfies the letter of an instruction while missing its spirit entirely. Formal verification is mechanistic. It will not save you from having asked the wrong question. What it will do is tell you, with unusual confidence, whether the answer to the question you did ask is actually correct.

There is a reasonable skeptic’s case to be made here, and Noah made it directly to Hartnett on the show: maybe Lean ends up like chaos theory, the subject of James Gleick’s Chaos — a genuinely important development that nonetheless settles, after the initial excitement, into being one subfield among many, ignored by the ninety percent of mathematicians who don’t happen to need it. It’s a fair comparison. Hartnett’s answer is that it misses the scale of what’s actually changing underneath it: not whether Lean itself becomes central, but whether some formal-verification layer becomes mandatory, because the volume of AI-generated mathematics is about to make ad hoc human checking impossible. The specific tool might be replaceable. The need for the category of tool, he argues, is not.

The most quietly persuasive part of the book is the part that seems, at first, like a detour: the story of Peter Scholze, one of the most accomplished living mathematicians, deciding to formalize a piece of his own work — not because he doubted it, but because he wanted to be sure. Through the process, he discovered that writing a proof in a language with zero tolerance for vagueness forced him to understand his own argument more precisely than he had before. That is the opposite of what most people assume formalization does to mathematical insight. It doesn’t flatten the art out of the work. Done well, it sharpens it.

This is, in the end, why the book resists being filed away as a story about a useful piece of infrastructure. It’s a story about what happens to understanding when you’re no longer allowed to skip the line you already know is true — and about the very particular, very human stubbornness of the people who decided that mattered enough to spend a decade proving it.