Kevin Hartnett on Lean, Mathematical Proof and the Limits of AI Verification

Journalist Kevin Hartnett joins Tim Scarfe to tell the story of Lean, the people who built it, and the changing role of proof in mathematics. Their conversation brings together mathematicians and computer scientists who disagree about what formal verification can provide, even as they share an interest in making mathematical reasoning more reliable.

The story begins with the Kepler conjecture: how densely can identical spheres be packed? Thomas Hales and Samuel Ferguson produced a proof that depended on extensive computation. Reviewing it placed an unusually heavy burden on mathematicians, who had to assess both a long argument and calculations that no person could practically check by hand.

The host describes how Hales and Ferguson reduced the sphere-packing problem to a large collection of cases. The proof combined mathematical reasoning with computer calculations to bound the density of each configuration. Its scale was precisely what made the completed argument so difficult to review.

When Hales sent the work to the Annals of Mathematics, the editors faced an unfamiliar refereeing problem. The reviewers could examine individual pieces and find them convincing, yet the entire argument included a sprawling body of calculations and computer code. Understanding how all the pieces supported the claimed conclusion was a different task.

As the review continued, Hales reconsidered plans to use the same methods on other problems. If mathematicians could not easily verify his existing result, applying similarly extensive calculations elsewhere risked producing more work that the community could not confidently absorb. Formal verification grew out of this practical problem of trust.

De Moura describes the subsequent formalization as a milestone predating Lean. Hales used existing proof assistants for the project, and the result showed that a major theorem mathematicians cared about could be checked with such tools. Hales's later choice to use Lean on other work mattered for Lean's visibility.

Mathematical proof has traditionally depended on a social process as well as logical argument: a researcher writes a proof, other specialists study it, and confidence grows through review and use. That process is powerful, but the participants in the discussion point out that the increasing length and complexity of proofs can make independent checking difficult.

De Moura argues that checkable proof certificates can support collaboration among people who have never met. A large project can be divided into smaller claims, and participants with different levels of experience can contribute. A project organizer still has to care whether the resulting work is understandable and maintainable.

Correctness is not the only thing mathematicians want from a proof. A proof can establish that a result follows from its assumptions without giving a reader the conceptual insight that makes the result illuminating. Formal checking addresses part of the problem; understanding why an argument works remains a separate concern.

Hartnett distinguishes settling a question from developing methods that open up new areas. A computational proof can be legitimate even if it does not provide the same conceptual tools as a more abstract argument. Paul Lessard returns to the need for an account a person can understand: getting an answer and grasping why it is right are different goals.

Formalization takes time. Hartnett describes the Kepler effort as roughly twenty person-years and notes that the ratio of formal code to informal mathematics can be high. For a mathematician who already trusts a familiar result, spending that effort merely to check it may seem less rewarding than pursuing a new discovery.

Lean is both a programming language and an interactive theorem prover. A user expresses definitions, statements and arguments in a precise language; Lean checks whether a proof meets the stated claim. It does not simply read an ordinary mathematical paper and decide whether its argument is sound.

A small kernel helps isolate the portion of the system that must be trusted. De Moura explains that accepting an invalid proof is more serious than rejecting a valid one: the latter blocks progress, while the former can let false results support further claims. A small checker also makes independent implementations more feasible.

Leonardo de Moura had previously worked on the Z3 solver and wanted tools that could help people reason about the correctness of software. Lean grew out of that interest. Proving a specific property of a program is different from proving that the program has no bugs of any kind: the strength of the guarantee depends on what was stated and checked.

Z3's success also showed de Moura the limits of automated theorem proving. Automated solvers are powerful within the classes of problems they can handle, but he wanted a richer language in which people could guide the construction of arguments. Lean's interactive approach gave human users a more active role in assembling proofs.

Hartnett frames the book as the story of a tool initially motivated by software verification that mathematicians adopted for their own purposes. That shift was not automatic: it required a community to develop a library and work through the different demands of software verification, mathematical research and education.

Jeremy Avigad describes a design choice beneath the mathematics. Lean uses dependent type theory, which lets definitions and proofs be expressed in a language with a rich structure. Such foundations offer useful ways to organize reasoning, but those benefits have to be balanced against the complexity of learning, implementing and maintaining the system.

De Moura initially preferred a simpler logical foundation, which he thought would be easier to implement and sufficient for many verification tasks. Avigad argued that dependent type theory was better suited to the networks of algebraic structures used in modern mathematics. The choice was negotiated among people with different experiences of what a proof assistant needed to do.

Avigad had worked with both Isabelle and Rocq. He praises Isabelle's automation, while explaining that some kinds of abstract algebra were easier to express in a more powerful type system. That expressiveness had a price: dependent type theory was harder to implement and introduced more corner cases for users and developers.

In 2013, de Moura chose dependent type theory for Lean. He later saw the mathematical library's abstractions prove useful even for software verification, including cryptography. In his telling, the added early work paid off because the system could serve both mathematicians and people proving properties of programs.

Hartnett describes de Moura as a researcher without a large engineering team, trying to respond to a growing group of users. Mathematicians loved the tool and asked for features; de Moura wanted to help, but support requests competed with time for his own longer-term vision. Those competing demands became a source of frustration.

Mathematician Kevin Buzzard became interested in Lean after thinking about how difficult it can be to know exactly which results in the literature are fully established. His concern was not that mathematics is generally worthless, but that an accepted paper can leave details implicit, and that checking the gaps is demanding human work.

When Buzzard first explored proof assistants, much of the formalized material was elementary. That could be disappointing if the goal was to check frontier research, but he also found the process fun. The question became not only whether a machine could find an error, but how much mathematics a community could teach the software to express.

His concern about gaps applied to papers building on a fast-moving field, rather than a claim that Scholze's own foundational work was sloppy. Buzzard wanted to turn arguments into formal language, identify missing details where necessary and build confidence that subsequent research could depend on them.

That library became mathlib, a collaborative collection of definitions and theorems built by Lean users. Contributors do not merely put isolated proofs into a box. They have to decide how concepts should be represented so that results from different areas can interact and later contributors can build on them.

Hartnett compares the creation of mathlib to a barn raising. Contributors built basic definitions and results from the ground up, making them available to others. A proof assistant may have logical rules, but without such a library, every user would have to rebuild too much of the mathematical background for a serious project.

Buzzard recalls contributing work on complex numbers and involving students in formalization. What might seem like routine background to a mathematician must be described precisely enough for the checker. That effort can expose choices that a paper leaves invisible, and it gives newcomers concrete ways to participate in a shared mathematical project.

Buzzard organized students to contribute material they were studying as undergraduates. He describes the library almost as a student itself: teach it the definitions, prove basic facts and then move on to the next subject. Other groups were doing the same around the world, so knowledge accumulated as shared infrastructure.

The maintainers also had to decide when an idea was mature enough for that infrastructure. Buzzard says a promising frontier concept may still be changing, while a shared library benefits from definitions that are well understood and useful at the right level of generality. Changing a fundamental definition later can break thousands of dependent files.

Buzzard first helped formalize schemes to show mathematicians that Lean could express sophisticated geometry. When colleagues dismissed schemes as established rather than frontier mathematics, the team chose a newer target: Scholze's perfectoid spaces. Buzzard, Patrick Massot and Johan Commelin mapped the intermediate definitions needed to reach that target.

Hartnett describes the resulting library as having a broad foundation with narrow towers reaching into the research frontier. A successful formalization of an advanced definition does not mean every neighboring subject has been built out. It does show that the basic language and enough supporting material can reach a demanding modern object.

Buzzard recalls watching Hales give a streamed talk about formalizing modern mathematics. Hales proposed starting with the statements of theorems, rather than demanding that every mathematician encode an entire proof. Writing a precise statement is a smaller task and still gives readers a clear account of what has been claimed.

Buzzard illustrates the problem with a paper that declares in an early section that a prime p is at least five, then states a theorem much later using p. Someone who starts reading at the later section may miss the restriction. Encoding the statement explicitly forces the author to decide which assumptions belong in it.

Definitions can be comparatively short even when the theorems built on them require enormous proofs. For Buzzard, that made Hales's proposal a viable bridge between elementary library material and research papers. He later obtained support for a project translating recent theorem statements; he says the work was around one-fifth complete at the time of the interview.

Hartnett explains why the work can be unexpectedly tedious. A step a human regards as obvious still has to follow from definitions and previously established facts. The difficulty is not that mathematicians doubt simple arithmetic, but that the computer needs the intermediate justification in a form it can check.

Lean's tactics automate familiar patterns of reasoning. Instead of manually supplying every routine arithmetic step, a user can invoke a helper that constructs the necessary proof. De Moura built some tactics and enabled community members to write others, reducing repetitive work while retaining the kernel's role in checking the result.

In 2020 Scholze contacted Buzzard about a specific theorem in a recent preprint. Buzzard had participated in a study group that read the paper, but when he looked back at the requested proof, he realized the group had skimmed its six pages of technical calculations. Other specialists Scholze had asked gave similar answers.

Scholze thought much of the material might be expressible using mathematics the library already knew. Buzzard saw a chance to test Lean on a current result, though the community was small and the proof was demanding. With Scholze's agreement, he made the challenge public, attracting people willing to contribute substantial time.

As the group read the proof closely, Commelin found a simplification that shortened the work. Six months later the team had checked the central claim. Buzzard says the result reassured Scholze and offered a more conceptual argument for part of the proof: the formalization had helped people understand the mathematics as well as check it.

The project's visibility brought new mathematicians to Lean. An expert might ask whether the library could immediately handle a latest theorem and learn that the basic objects in that field still had to be developed first. Those conversations nevertheless helped the community extend the library into more areas.

Hartnett points to another benefit of a formal proof: a reader can inspect how its components connect instead of treating an article as a static sequence of assertions. A proof assistant can make dependencies explicit and let a reader navigate from a claim to the ingredients on which it relies.

The participants ask whether an AI beginning with mathematical axioms would rediscover the subjects humans have chosen to develop. Hartnett recounts mathematicians' speculation that such a system might diverge very early. Humans favor definitions and abstractions that feel meaningful and useful, while a search aimed solely at valid statements need not share those preferences.

Mathematical problems are also attractive for reinforcement learning because a correct solution can provide a relatively clear feedback signal. Hartnett describes the International Mathematical Olympiad as a challenging target: its problems use school-level prerequisites but require unusually sophisticated reasoning.

At the 2024 Olympiad, DeepMind used AlphaProof on formally expressed problems and produced Lean proofs for checking. DeepMind’s combined systems reached a silver-medal level, but had more time than human competitors and substantial computing resources. Lean checking also supplied feedback during AlphaProof training.

AlphaProof could not directly consume every competition question as an ordinary reader would. Translating natural-language problems into formal statements was a separate challenge. Equations made some algebra and number-theory questions easier to formalize, while combinatorics questions expressed as stories posed a harder translation problem.

In the Equational Theories project, Terence Tao organized a large collaboration to map implications between algebraic laws, using Lean to check results. The participants reduced a space of roughly 22 million questions to a few hundred and then a handful of stubborn cases. The point was broader than completing a table: the project tested a collaborative, exploratory way to do mathematics.

Tao compared the effort to experimental work in physics. Large-scale computation and collaboration can uncover structures worth studying without replacing theory. The participants describe finding unexpected constructions along the way, illustrating how a search through unfamiliar territory can suggest questions that were not the original target.

In 2025, DeepMind and OpenAI also reported gold-level Olympiad results using natural-language proofs, rather than Lean verification of those answers. Hartnett expects both approaches to matter: formal environments can supply feedback for training and help sift large numbers of attempted arguments, while natural-language systems may be useful for producing explanations mathematicians can assess.

Buzzard sees a tension between fast formalization and the design principles behind mathlib. The library's maintainers seek abstractions that make later work easier. An AI system can instead push through a long, awkward translation that checks, without necessarily stopping to ask whether the underlying definitions are organized in the most useful way.

The new tools can help with maintenance too. Buzzard imagines an AI adapting many dependent proofs after a foundational definition changes. But he says that the existence of an automated repair mechanism does not remove the library's need for conceptual clarity: maintainers still have to decide what should be admitted and how it fits with the rest.

Hartnett notes that AI can lower the barrier of Lean syntax and may let more mathematicians use the system. Autoformalization also raises the possibility of translating material from papers and textbooks much faster. Yet a flood of code shifts work onto the people responsible for checking its quality and integrating it into a coherent library.

A proof checker answers whether a derivation establishes the formal statement it was given. It cannot itself guarantee that the statement captures what a mathematician meant. If an AI formalizes the wrong target or omits an intended condition, a perfectly valid Lean proof can still leave the human question unanswered.

Buzzard argues that ordinary mathematical writing is not always as explicit as its reputation suggests. Experts often understand an unstated assumption from context. When a statement has to be translated into a formal language, the translator must decide whether to encode the words on the page literally or supply what readers normally infer.

He describes a project formalizing statements of 50 theorems in the Annals of Mathematics. According to his account, an AI review found both mistakes introduced during translation and cases where the published wording left out assumptions that specialists would treat as obvious. The example concerns the precision of the stated claims, not a blanket verdict that the underlying mathematical ideas were wrong.

Avigad recalls that early arguments for proof assistants, framed mainly around catching errors, did not persuade many mathematicians. Their first loyalty is to ideas and understanding. Rigor is the medium in which those ideas can be expressed and checked, but a list of mechanically verified steps is not by itself the insight that makes a proof valuable.

Formalization can nevertheless create understanding of its own. Avigad compares building a mathematical library to designing software interfaces: one must choose what a definition exposes, how separate modules fit together and which assumptions are needed for them to interact. Returning to familiar mathematics under those constraints can reveal its structure in a new way.

The Liquid Tensor work exposed a similar question about definitions. Scholze worried that Lean could validate an argument about a formally defined object while the formal definition failed to capture the object mathematicians intended. A definition is not correct merely because it is syntactically well formed; people must judge whether it is the right representation for their purpose.

Commelin and collaborators responded in part by writing concrete examples, like unit tests, for important definitions. Examples cannot prove that a definition captures every intended feature, but they can show whether it behaves as expected in familiar cases. The discussion presents testing as a source of reassurance alongside, not a substitute for, mathematical judgment.

De Moura also describes the human cost of maintaining a shared project. Ideas can be easy to propose and expensive to evaluate: a maintainer finds a flaw, the proposer revises the idea, and each subsequent review takes more time. As a system grows, that asymmetry makes focus and careful review important resources.

A Lean implementation of the zlib compression format offers an example of both AI assistance and the limits of specifications. The discussion describes translating an implementation, running its tests and proving a round-trip property: decompressing compressed data returns the original input. That is a useful property, but it is only one property of the desired system.

De Moura gives a simple counterexample to an incomplete specification. If the only requirement is that compression followed by decompression returns the input, both functions could simply return their input unchanged. The stated property would hold, but nothing would be compressed. Additional tests and properties narrow the gap between what was checked and what a user actually wants.

That gap matters for AI-generated software because writing a complete specification can itself be difficult. The participants consider whether AI might help write specifications as well as code, and whether verification can relieve the growing bottleneck of reviewing generated programs. Hartnett describes this as an active bet rather than an established solution.

Buzzard is optimistic that AI and formal tools will accelerate mathematics, discover more theorems and open up unfamiliar areas for exploration. Other mathematicians react with concern or grief as their subject changes. The conversation leaves the pace and consequences of that change uncertain, rather than assuming everyone values the same outcome.

Avigad puts the human question at the center: what goals do people have, and how should they use these systems to pursue them? A server that proves results on its own is less interesting to him than the way people interact with it and the understanding they gain through that interaction.

Hartnett says that reporting the book brought an ethical responsibility to the people whose life's work he was describing. He interviewed key figures repeatedly and drew on a substantial record of email and Zulip discussions, reconstructing the decisions and relationships behind the software rather than treating Lean as a tool that appeared fully formed.

He found that a period of tension had separated de Moura's work on Lean 4 from parts of the math community that continued developing mathlib. Different visions and strong personalities contributed to the friction. Participants describe a close community with real disagreements, rather than a story that can be reduced to heroes and villains.

Avigad remembers reconnecting with de Moura during a visit to Seattle: they took time away from a meeting and walked together, talking about Lean and other things. Looking back on the early days, he says the project's growth has been surreal. Scarfe closes by recommending Hartnett's account of the people and persistence behind it.