After the Proof Checks: Kevin Hartnett on Lean, AI, and Mathematical Understanding

1. Guest Background

Kevin Hartnett joins Machine Learning Street Talk as the author of Proof in the Code, a book about computer-assisted mathematics and the people building its infrastructure. Beginning with the computational proof of the Kepler conjecture, the book follows Lean's creator and collaborators as their software becomes a medium for mathematical work. The episode, hosted by Tim Scarfe and co-hosts, runs approximately ninety-four minutes and combines Hartnett's account with contributions from participants including Leo de Moura, Kevin Buzzard, and Jeremy Avigad.

Hartnett's relevant experience is sustained reporting on this community. He says a 2020 Quanta Magazine assignment about Mathlib first drew him into its development. For the book, he spent substantial time with six or seven central sources and worked through shared private emails, public Zulip threads, and private messages made available to him. That reporting gives the conversation access to design negotiations and working relationships alongside technical explanations.

His perspective matters because the episode is examining how a practice changes, rather than presenting a single new theorem. Hartnett connects the history of proof checking to questions about mathematical value and AI. The developers and mathematicians supply complementary accounts of what they wanted the tools to do, what building them required, and where verification still leaves human judgment indispensable.

2. What the Episode Covers

The Kepler conjecture supplies the episode's opening difficulty: a proof can become too computationally extensive for ordinary review to establish confidence in the whole. In the account presented, Hales and Ferguson reduced the sphere-packing problem to many computational checks. Reviewers found the portions they examined convincing, yet struggled to establish whether the calculations embedded in code collectively delivered the claimed result. De Moura recalls Hales subsequently using HOL Light and Isabelle for formalization. The issue was how to produce something that could be checked systematically across the entire argument.

Hartnett contrasts that aspiration with the social mechanisms supporting everyday mathematics. Readers bring background knowledge, familiarity with authors, and a sense of how arguments should work; they do not routinely reconstruct every inference. De Moura explains the collaborative consequence of checkable certificates: contributors who have never met can supply pieces of a project without requiring its organizer to repeat every correctness check manually. Planning the pieces and making the resulting proof maintainable remain substantial human work.

Lean provides both a programming language and a proof assistant. The episode distinguishes its logical foundation, which determines expression and inference, from the kernel that checks adherence to those rules. De Moura advocates keeping that kernel small enough to make independent checking realistic. An erroneous acceptance is especially serious because later arguments can build on the false statement. Around this checking process, extensible tactics automate repetitive proof steps, reducing the work required to make elementary reasoning explicit.

The conversation also explains why Lean's foundations involved a difficult tradeoff. Hartnett describes its origins in a desire for software verification with a richer expressive language than Z3. Avigad argued that dependent type theory would better support the complex networks of structures used in modern mathematics. He also acknowledges the price: a more difficult implementation, a harder language to use, and additional corner cases. Expressiveness required deliberate investment.

Mathlib made that expressive framework useful through accumulated definitions and results. Buzzard recalls adding complex numbers in 2017 and recruiting undergraduates to formalize their coursework. Roughly three years later, he says, the library covered most of their undergraduate curriculum. A subsequent dependency blueprint allowed Buzzard and collaborators to express perfectoid spaces, showing that a frontier object could be defined without claiming its surrounding theory had all been verified.

The episode then separates stating mathematics precisely from checking its proofs. Hales's proposal to formalize theorem statements could expose assumptions scattered across a paper, such as a prime being at least five. By contrast, Scholze's request concerned a key argument whose approximately six pages of calculations readers had skimmed. Buzzard recalls a simplification helping reduce an expected year of work to about six months, producing both verification and a more conceptual understanding of part of the argument.

3. Core Views: Reasoning, Examples, and Limits

The strongest argument running through the episode is that mathematical correctness, faithful expression, and understanding are separate achievements. Hartnett judges a contribution partly by whether it creates concepts and abstractions that support further work. His comparison between Hales's computational approach and Wiles's conceptual developments illustrates different kinds of mathematical value. He also allows that proofs unconstrained by interpretability can be useful. Settling a question matters, even when the route does not give humans a reusable way of thinking about adjacent questions.

That distinction helps explain resistance to formalization. Hartnett cites approximately twenty person-years for formalizing Hales's result, while the discussion invokes formal-to-informal line ratios of twenty to one or higher. These are cost descriptions supplied in the episode, not a general measurement established by this evidence. Their argumentative purpose is clear: for mathematicians already confident in a result, additional assurance can look less attractive than spending the same effort discovering something new. Improvements in conceptual organization or understanding offer a different return on that investment.

The formalization gap places a boundary around the assurance itself. A checker establishes that a target follows from specified assumptions and definitions. It does not independently establish that this target expresses the conjecture humans intended. A completely accepted proof can therefore answer the wrong question. Trust moves toward the decisions that precede checking: what the definitions mean, which hypotheses were included, and whether the formal statement corresponds to its informal source.

The theorem-statement project makes this boundary concrete. A participant reports that AI-assisted review of fifty Annals of Mathematics statements found both mistakes introduced during translation and conditions omitted from the original wording. Examples included requiring n to be at least three or a set to be nonempty. These findings concern literal expression. They do not establish that the intended results, understood with the conditions experts supplied, were disproved. The accompanying description of moving from 99% to 100% is a metaphor for making those conditions explicit, not a measured rate of mathematical correctness or AI reliability.

Formalization can also improve understanding through the work of representation. Discussants describe reconsidering encapsulation, modules, and interfaces when mathematical components must interact in a library. This forces attention to how concepts fit together. Yet a formally valid representation may still be a poor shared abstraction. Buzzard emphasizes mature mathematics at appropriate generality because changing foundational definitions can break thousands of files. AI may make repairing those dependencies easier while remaining indifferent to whether a cleaner conceptual organization would avoid the difficulty.

Hartnett's account of automatic formalization sharpens this tension. He says models can produce Lean versions of papers in a fraction of the time required by human teams, but the episode supplies no specific benchmark for that comparison. He also describes a flood of material whose precision, economy, or organization may fall short of Mathlib standards. Faster production can therefore increase the importance of review. Passing a checker does not settle whether a contribution belongs in a maintained public library.

The AI performance examples require similarly careful separation. According to the episode, AlphaProof's 2024 silver-medal-level result involved formal inputs, Lean proofs, additional time, and substantial compute compared with human contestants. The 2025 gold-level results discussed used natural-language proofs, did not rely on Lean to verify those competition answers, and had different grading arrangements. These are distinct demonstrations. Hartnett's reported approximately 80% near-perfect automatic formalization for algebra and number-theory questions is also task-specific; the greater difficulty of narrative combinatorics questions argues against treating it as a universal translation success rate.

Finally, the Equational Theories example broadens the measure of progress. The episode reports that Tao's collaboration reduced approximately twenty-two million implication questions to four remaining questions and encountered constructions including magma cohomology. Its significance in the discussion lies in organizing collaborative experimentation and using data to complement theory. That supports a possibility for machine-checked exploration. It does not establish that every mathematical field benefits equally from this approach, or that reducing a large problem count necessarily produces understanding.

4. Learning and Application

A research team can apply the episode's distinctions by defining separate deliverables for objects, statements, and proofs. Specify the intended mathematical object, make the theorem's assumptions explicit, and identify exactly which argument has been checked. The perfectoid-space definition, Hales's statement-first proposal, and the Scholze verification project illustrate different useful scopes. This approach permits progress when a complete proof is too expensive while keeping claims proportional to the work. Each deliverable should explain the correspondence between the mathematical intention and its formal expression so reviewers can inspect the question before relying on the answer.

For important definitions, concrete examples provide an additional review technique. Commelin and Topaz used examples as unit tests; a practical extension is to select representative cases, boundary cases, and objects that should be excluded. Such checks can expose a mismatch between the intended concept and its implementation. Their limitation must remain explicit: examples offer reassurance rather than decisive evidence of faithfulness. Passing them should lead to further examination of assumptions, quantifiers, and definitions, rather than closing that examination.

Software teams can turn specification review into an active search for degenerate implementations. The episode reports that Kim Morrison's Claude-agent Zlib project translated C into Lean, passed the original test suite, and proved round-trip recovery for arbitrary data and compression levels. The supplied material does not include artifacts for independent inspection. The discussant's identity-function example nevertheless provides a precise review method: ask what implementation could satisfy the stated property while defeating the purpose of the component. Returning the input unchanged in both directions passes round-trip recovery without adequately specifying compression.

The proposed additions involving output size or comparison with another implementation should be treated as candidate specification work. Teams must establish the relevant inputs, comparison conditions, and intended behavior before adopting them. The episode does not establish that the project proved those additions, or that every input must become smaller. A useful review record would distinguish tested behavior, proved properties, and requirements that remain unexpressed. This preserves the value of a narrow guarantee without expanding it into an unsupported claim of complete correctness.

The level of autonomy should also affect the release threshold. As the discussion observes, a human reading AI-produced code can identify problems outside the written specification. Development without code inspection depends more heavily on the specification covering the intended behavior. A bounded component with explicit inputs, outputs, and critical properties therefore offers a more tractable starting point than an unrestricted claim about a complex system. AI-generated specifications still require review against the human goal; otherwise, code and specification can omit the same requirement.

Library maintainers should account for understanding and review costs alongside generation speed. Requiring explanations of abstractions, dependencies, and reusable interfaces is one way to apply the episode's concern about material that checks but is difficult to maintain. The host's understanding-debt framing asks whether system growth is outpacing people's ability to comprehend it. AI-assisted specification writing and the proposed transfer from mathematical proving to software verification may help, but the respondent explicitly describes the latter as an uncertain bet. Bounded experiments, clear evidence of coverage, and continued human judgment about goals remain justified by the discussion.

Source

• Original episode: Mathematics Just Changed Forever — Kevin Hartnett