A new book tells the story of how a programming language conquered mathematics. Its most important chapter may be the one that hasn’t happened yet.
Kevin Hartnett’s book The Proof in the Code: How a Truth Machine Is Transforming Math and AI, published in June 2026, tells the inside story of Lean, the programming language that began as an obscure bug-checking project by a lone Microsoft (News - Alert) Research engineer named Leonardo de Moura and grew into what Hartnett calls a truth machine: a program that can provide a complete, 100% guarantee that a chain of logic is correct. The book chronicles how a crew of mathematical outsiders adopted Lean with missionary zeal, how two of the world’s most prominent mathematicians staked their reputations on it, and how the AI labs eventually arrived to train their systems on its libraries.
Hartnett wrote the proof in the code, the story of mathematics being rebuilt inside a programming language. The sequel the field is now attempting is the proof of the code: the same machinery of certainty, turned on software itself.
How Lean upended mathematics
For all of its history, mathematics was checked the way it was written, by people. Referees read proofs, and the field accepted a result when enough experts vouched for it. Lean replaced the referee with a machine that verifies every step, and the mathematicians who embraced it did so precisely because human checking had reached its limits.
In December 2020, the Fields medalist Peter Scholze challenged the Lean community to verify the central theorem of his theory of liquid vector spaces, a result he worried contained an error too deep for human referees to find; six months in, he called it “absolutely insane” that proof assistants could verify difficult original research so quickly. The Liquid Tensor Experiment was completed in 2022. Terence Tao went further, coordinating crowdsourced formalization projects, including one that settled all 22,028,942 implications among 4,694 equational laws, and emerged an evangelist for a machine-checked style of mathematics in which strangers can collaborate because the computer guarantees correctness.
The result is Mathlib, a community-built library of formalized mathematics running to millions of machine-verified lines, and a cultural transformation Hartnett documents in detail: a multi-thousand-year-old discipline changing how it decides what is true.
The AI labs noticed, because a library of formal mathematics is also training data; DeepMind’s AlphaProof learned to prove theorems in Lean by auto-formalizing informal mathematics at a scale no human team could have attempted.
The next chapter
The investor and philanthropist Chris Hsu, founder of Kilometre Capital and Rocketeer Management, whose Infinitude Foundation includes the Lean Focused Research Organization among its grantees, is one of many now asserting that the revolution that proved the math should now prove the software.
The people who built the original truth machine are already writing the next chapter. In April 2026, de Moura announced Signal Shot, a public moonshot to formally verify the Signal messaging protocol and its Rust implementation in Lean, co-led by Signal, the Beneficial AI Foundation, and the Lean FRO, and modeled explicitly on the Liquid Tensor Experiment: the same test of whether Lean scales, posed this time for deployed software rather than frontier mathematics. Amazon, announcing what it called the largest donation in the Lean FRO’s history, framed the language’s purpose the same way: mathematically proving that software, and AI agents, behave as specified for all inputs, not just the tested ones.
The infrastructure is being laid deliberately. CSLib, introduced in February 2026 by a team whose steering committee spans Stanford, Amazon, Google (News - Alert) DeepMind, and the Lean FRO itself, aims to be for computer science what Mathlib became for mathematics: a shared, machine-checked library of the field’s knowledge, built to support both human and AI engineering of large-scale verified systems. The parallel is explicit in the project’s own framing. Mathlib’s history suggests how such libraries compound. What begins as a curiosity can become a commons, and the commons becomes the substrate for work nobody could have attempted alone.
Why does software need this at all? Because the conditions that pushed mathematicians to Lean, proofs too large and consequential for human checking, now describe code. AI systems are writing software faster than humans can review it, and finding flaws in existing software faster than humans can patch it; after a single month of Project Glasswing, Anthropic reported that the binding constraint on software security had already moved from finding vulnerabilities to verifying, disclosing, and patching them. Hsu has argued that this is precisely the moment the economics flip: AI-enabled auto-formalization is collapsing the specification and proof labor that kept verification a specialist craft, so the discipline can finally be deployed at the scale of software itself.
Hsu has argued that de Moura’s contribution may therefore extend far beyond mathematics. By creating Lean, he helped build an infrastructure through which machines can establish correctness rather than merely predict it. As AI increasingly writes the software controlling financial systems, communications, infrastructure, and eventually autonomous machines, that distinction becomes a matter of human security: Lean provides a foundation for proving that critical systems do what humanity intended them to do, rather than simply trusting that they will.
What proof still cannot prove
Hsu is careful to note two caveats sitting alongside the enthusiasm. First, mathematics was in one sense the easy case: theorems do not have messy interfaces with hardware, networks, and human intent, and a formal specification of a mathematical statement is usually uncontroversial in a way that a specification of a payments system is not. A proof of the code guarantees the code matches the specification; it cannot guarantee the specification matches the world. Second, the scale gap is real. The celebrated verified artifacts remain small relative to the systems civilization runs on, and skeptics rightly point out that assurance has never been demonstrated at scale.
But in 2019, the idea that Fields medalists would formalize frontier research in a proof assistant was fanciful; by 2026, it was a book with substantial impact across mathematics. Revolutions in what can be checked have a way of arriving through the same sequence, skepticism, curiosity, infrastructure, and then suddenly a new normal. The proof in the code took a decade and changed mathematics. The proof of the code is now being drafted, in public, by many of the same hands, and there is a reasonable case that it will be the more consequential of the two.
The remaining problem is intent
For Hsu, the transition from the proof in the code to the proof of the code leaves one critical problem unresolved: who specifies what the software is supposed to do? As constructing and checking proofs becomes increasingly tractable, the hard problem moves upstream to capturing human intent. A machine can prove perfectly that code matches a specification without proving that the specification says the right thing.
That problem becomes more acute in an AI-native development stack. If the same AI interprets a request, writes the specification, generates the code, and constructs the proof, one misunderstanding can propagate through every layer and emerge labeled “verified.” Hsu argues that the critical trust boundary therefore shifts from code and proof to intent: the user expresses intent in natural language, that intent is made precise and reviewable, and formalization and proof happen underneath.
This reframes an older objection to formal verification: that trust ultimately depended on humans reviewing work that machines could not meaningfully validate. Machine-checked mathematics, as Hartnett chronicles, has changed that premise. Now AI is accelerating the same transition in software just as it produces more code than humans can plausibly review. The emerging architecture is simpler: humans establish intent; machines write the code and check the proof. The remaining question is whether we asked them to prove the right thing.
Hsu makes the same distinction in responding to Ivan Gavran’s August 2026 essay, The Case Against Formal Verification, 50 Years Later, which revisits DeMillo, Lipton and Perlis’s 1979 critique of program verification in Communications of the ACM. Gavran concludes that AI is weakening many of the historical objections to formal verification while leaving one especially important problem intact: translating messy human requirements into the right specification. Humans, in his account, remain the final arbiter of what “correct” means. Hsu argues that this is now the crux. Machines can increasingly write code and check proofs cheaply; the scarce source of trust moves upstream to capturing intent correctly. For Hsu, the decisive layer is therefore the interface between human intent and formal specification: humans establish what must be true; machines can increasingly handle the rest.
Where human trust goes next
Hsu has framed a larger arc connecting Hartnett’s story to what comes next. Mathematics moved from trusting humans to check every step of a proof to trusting machines to verify those steps. Software may now be undergoing the same transition: AI writes the code, formal methods prove that it satisfies its specification, and human attention moves to the one place machines cannot independently settle: what we actually intended the system to do.
If that transition succeeds, the most important consequence of Lean may not ultimately be that it changed how mathematics establishes truth. It may be that it supplied the architecture for how an AI-written world establishes trust: humans specify the intent; machines build the software; proofs establish that the two match.
