Mathematics Just Changed Forever — Kevin Hartnett

Summary

• AI mathematics is advancing through both formal and natural-language routes. Hartnett contrasts AlphaProof’s 2024 silver-medal-level IMO performance, using Lean and substantial compute, with the gold-level natural-language results reported by Google DeepMind and OpenAI in July 2025. Lean still supplies a valuable training and filtering mechanism when models generate many candidate proofs: “Lean can tell you which ones those are.”
• The adoption hurdle has been the cost of formalization relative to its perceived payoff. Hales spent twenty person-years formalizing Kepler’s conjecture; the de Bruijn factor can require twenty or more lines of formal code per informal line. Mathematicians principally want “discovering new math,” making automation and improved understanding stronger adoption arguments than correctness assurance alone.
• Autoformalization shifts scarce effort toward library design and maintenance. AI can translate papers into Lean much faster than human teams, but checked code can still use cumbersome definitions and weak abstractions. Hartnett calls the influx “a little bit of a Trojan horse”; Buzzard expects larger AI-generated libraries while maintaining that mathlib must preserve conceptual quality.
• Machine verification moves the trust problem upstream into definitions and specifications. Buzzard’s team formalized fifty Annals theorem statements, then used AI to find both translation mistakes and missing assumptions in published statements involving four Fields Medalists. These were cases where experts understood the intended meaning, but the literal statement was false: “obviously, n had to be at least three.”
• Formalization can improve understanding and enable new discovery. Checking Scholze’s six-page argument produced a conceptual simplification and resolved his concern that nobody had carefully read it: “something has now actually finally read it.” Separately, Tao’s collaboration reduced twenty-two million implication questions to four remaining cases while uncovering unfamiliar mathematical constructions.
• AI code verification offers a potential application, conditional on specifying the right behavior. A compression program can satisfy a round-trip proof simply by returning its input unchanged; correctness of the proof does not establish useful compression. Avigad notes Harmonic’s bet that mathematical proving capabilities will transfer to software verification, while Buzzard preserves the uncertainty: “Whether or not it pans out, I don’t know.”

Deep dive

1. A proof can settle a question and still overwhelm peer review

• Scarfe opens with Kepler’s conjecture: the pyramid arrangement of oranges appears maximally dense, at about 0.74. Thomas Hales and Samuel Ferguson reduced the problem to configurations; Hales ultimately had 1,767 computer programs, with cases becoming harder as their densities approached the bound. Finishing in summer 1998 settled the computational work without settling how others could verify it.

• Hartnett describes the Annals of Mathematics confronting a sprawling calculation buried in code. Everything reviewers examined appeared correct, but they could not establish how the entire structure hung together. De Moura recalls acceptance with a disclaimer expressing something like 99% confidence. Hales subsequently formalized the result using HOL Light and Isabelle, before Lean existed.

• The distinction Hartnett preserves is between legitimacy and mathematical fertility. Hales settled the question, but his relatively elementary computational methods did not create broadly useful concepts comparable to those developed around Wiles’s Fermat proof. Lessard wants more than reliable answers: “I want to know why it comes up with a particular answer. I want the reason.”

• The economics explain resistance: Hales invested twenty person-years in formalization, while the de Bruijn factor often runs twenty formal lines per informal line, or higher. For mathematicians already confident a result is correct, that additional assurance can seem less valuable than new discoveries. Ordinary checking instead relies substantially on social trust and familiarity with existing mathematics.

2. Lean concentrates trust in a small kernel

• Hartnett traces de Moura’s earlier success to Z3, begun amid duplicated theorem-proving efforts at Microsoft around 2006. It could represent software pathways through variables and rule out combinations corresponding to particular bugs. Hartnett credits it with saving Microsoft hundreds of millions of dollars and winning automated-prover competitions, but its limited expressiveness left de Moura dissatisfied.

• Lean combines a programming language with an interactive proof assistant; it is itself implemented in Lean. Users can write programs, state properties, and construct mathematical proofs. Its logical foundation determines what statements mean, while a checker called the kernel verifies the resulting derivations. De Moura’s deliberately narrow assurance is: “we only trust the kernel.”

• That boundary matters because Lean as a whole “has zillions of bugs.” A kernel accepting a false statement is much worse than rejecting a true one: falsehood can propagate through subsequent proofs. The episode notes historical kernel bugs in Agda, Coq, and Isabelle. De Moura favored a minimal kernel, influenced by HOL Light, so independent implementations could check certificates.

3. Mathematical users won the foundational design argument

• Avigad had worked extensively with Isabelle and praised its automation, but found simple type theory limiting for modern mathematics’ interlocking algebraic structures. After his own year working with Rocq, he concluded that dependent type theory suited that mathematics. Separately, de Moura says he spent a sabbatical year in 2009 and 2010 working on formalizing the Feit–Thompson theorem.

• Avigad acknowledged the trade-off—“with great power comes great responsibility”—including implementation difficulty, usability problems, and corner cases. In summer 2013, de Moura chose dependent type theory, giving Avigad confidence that Lean could become useful for substantial abstract mathematics.

• De Moura says the additional work paid off beyond pure mathematics. Cryptography and differential privacy also require strong mathematical libraries. His former colleague Cédric Fournet later told him mathlib supplied “the right abstractions I need for verifying cryptography.” Supporting demanding mathematical users helped create abstractions useful to the software-verification users Lean originally targeted.

4. A shared library made Lean useful beyond elementary demonstrations

• Buzzard’s route began with a research crisis. Returning to hard mathematics after raising three children, he struggled with gaps and mistakes in literature surrounding the p-adic Langlands program. His criticism targeted work built upon Scholze’s discoveries, rather than Scholze’s own rigorous work. Without concrete applications to test against reality, he worried that unchecked abstractions could form a “house of cards.”

• Early mathlib contained about thirty thousand lines and basic undergraduate material, with real numbers only recently available and complex numbers absent. Buzzard contributed the latter—“complex numbers copyright 2017 Kevin Buzzard”—then recruited undergraduates to formalize what they were learning. Roughly three years later, the library knew most of the material taught in their undergraduate degrees.

• Hartnett describes a “spirit of a barn raising,” with contributions from Commelin, Massot, Avigad, Carneiro, Buzzard, and others. De Moura compares Commelin’s large projects to software engineering: an architect divides work into pieces that unfamiliar collaborators, even high-school students, can complete. Machine checking removes the need to manually establish every contributor’s proof correctness.

• Tactics reduce the accompanying drudgery. Hartnett recounts early difficulties formalizing even apparently obvious arithmetic; helper programs automate recurring arguments while producing proofs for checking. A ring tactic, for example, constructs an algebraic-identity proof until Lean reports “no goals.” De Moura also enabled users to write tactics themselves, allowing the community to expand Lean’s capabilities.

5. Formal statements offered a cheaper route to the frontier

• Buzzard first hoped formalizing schemes would establish Lean’s relevance, but mathematicians dismissed them as decades-old material. Around 2018, Buzzard, Massot, and Commelin instead targeted Scholze’s perfectoid spaces, building the definitions needed to express them. Hartnett calls this a “narrow skyscraper to the frontier”: mathlib broadly reached roughly first-year graduate mathematics, with some undergraduate gaps and isolated advances far beyond it.

• Hales proposed a less expensive entry point than translating entire proofs: formalize theorem statements. Buzzard’s example explains why that matters. Section 3 may establish that a prime p is at least five, while a theorem in section 7 simply mentions p. A reader entering there can miss the inherited hypothesis and misunderstand what has actually been proved.

• Buzzard initially recognized that checking modern papers wholesale was impossible, whereas defining objects and stating claims looked viable. Hales pushed the idea in 2017; seven years later, Buzzard wrote a grant proposal pursuing it. After a year, his team was about 20% through its selected recent top-journal statements, and he expected substantially more progress over the following year.

6. Scholze’s unread argument supplied the breakthrough

• In November 2020, Scholze asked Buzzard whether he had carefully read a recent preprint. A London study group had spent a term on it, but a follow-up question exposed the gap: they had skimmed a six-page technical proof, possibly theorem 8.4. Scholze had received similar answers from Princeton and Harvard: “that’s what everybody says.”

• Scholze and coauthor Dustin Clausen believed the argument worked, but Scholze worried that nobody else had checked it closely. Because much of the technical material was ultimately undergraduate-level, Lean might be capable of verification. The community initially anticipated a year’s work; Commelin found a simplification, and the key argument was checked in six months.

• The result offered more than reassurance. Buzzard recounts Scholze’s excitement that formalization had revealed a more conceptual argument and that “something has now actually finally read it.” Avigad connects this benefit to thinking about mathematical “APIs”: how concepts are packaged, which information is exposed, and how independently developed components interact.

• Publicity attracted professional mathematicians whose immediate question was whether Lean could handle their latest theorem. Often the answer remained no, but they could build their area’s foundations. COVID also accelerated participation: formalization combined engaging mathematics with the appeal of a computer game, while interactive proofs allowed investigation that static PDFs could not.

7. AI progress is outgrowing a single verification architecture

• Hartnett explains mathematics’ appeal as an AI training environment: a clear correctness signal supports reinforcement learning. AlphaProof needed Lean statements, however, while competition problems arrived in natural language. DeepMind reportedly autoformalized about 80% of algebra and number-theory questions nearly perfectly; story-like combinatorics proved harder. The resulting training supply reached tens of millions of formalized problems.

• For the 2024 IMO, AlphaProof received questions after the human competition, used more time and massive compute, and achieved a silver-medal-level score. Lean supplied verification during both reinforcement learning and competition problem solving. The comparison therefore preserves the achievement alongside the unequal resource conditions; it was not an identical sitting of the human examination.

• In July 2025, Google DeepMind and OpenAI reported gold-level IMO results using natural-language proofs. Google’s result was officially graded by the IMO; OpenAI’s was separately evaluated. Neither relied on Lean to verify those answers. Hartnett nevertheless expects both approaches: expressive models can generate arguments, while Lean can rapidly filter large numbers of candidate proofs.

• The episode’s September 2026 update reports that, in Epoch AI’s fixed-budget test, a prerelease OpenAI model proved Erdős problem 126 and refuted problem 74 by counterexample, both checked in Lean: two of 68 problems, versus none for four other models. It also mentions OpenAI’s September 8 claimed Navier–Stokes Millennium Problem resolution with Lean, “not under the best circumstances,” while placing that story outside scope.

8. Exhaustive exploration can uncover unfamiliar mathematics

• Tao launched Equational Theories in September 2024 to map implications among algebraic laws, using Lean to check results. Within a month, twenty-two million questions had narrowed to 238; by late November, 138 remained. By the end of March, four had resisted progress for several weeks. Settling every implication, however, was never the project’s sole objective.

• Tao envisioned an experimental branch of mathematics analogous to modern physics: large collaborations and extensive data complementing theory. Exploration uncovered constructions including magma cohomology. John Baez, who had initially called the project a “colossal waste of time,” acknowledged that he had never encountered it. To Tao, this was evidence for discovering “math from Mars.”

• Hartnett also recounts a speculative discussion with three mathematicians about starting AI from axioms, AlphaZero-style. Their expectation was that it would not necessarily rediscover more than the rational numbers before diverging from human mathematics. Their reasoning concerned abstraction: human researchers select concepts that feel satisfying, useful, and expansive, whereas correctness-driven search need not share those preferences.

9. Autoformalization creates a maintenance bottleneck

• AI can lower two barriers Hartnett identifies: learning Lean’s fiddly syntax and manually expanding its mathematical library. Agentic coding can help mathematicians express proofs without mastering every language detail. Beyond that, autoformalization promises textbook-scale translation; Hartnett says papers can now become Lean code in a fraction of the time previously required by human teams.

• The complication is canonical quality. Mathlib wants “polished mathematics”: well-understood concepts expressed at useful generality, with definitions that support future work. Changing a foundational definition can break thousands of files. An influx of formally valid but awkward material therefore creates substantial review and integration work, rather than automatically enriching the shared library.

• Buzzard observes that AI is happy to “just plow through” constructions humans would redesign. It could also repair downstream breakage after foundational changes. He expects AI-developed libraries to emerge within a year that are more poorly thought out in those terms. Mathlib’s maintainers still require conceptual quality; pouring tokens into the problem does not resolve their different objective.

10. Checked proofs move trust upstream to definitions

• Scarfe states the limit directly: “a checked proof can still be a proof of the wrong thing.” Someone must establish that a formal conjecture captures the intended definitions and assumptions. The kernel checks the derivation; it does not certify the human choice of target. “The trust has basically moved upstream.”

• Buzzard’s team translated fifty Annals theorem statements, then asked AI to check them before publication. It found both team translation mistakes and cases faithfully reproducing defective published wording. Four Fields Medalists were involved in statements that were literally false because assumptions such as n being at least three, or a set being nonempty, had been omitted.

• Buzzard describes a change of mind: a few years earlier, he would have said experts wrote exactly what they meant. Now he sees formalization exposing the gap between expert interpretation and literal expression. His “ninety-nine percent to a hundred percent” framing concerns making those implicit conditions explicit, rather than declaring the intended underlying results overturned.

• Scholze’s concern reaches deeper: how can anyone know a Lean definition matches the mathematical object intended? “Mathematics remains a human activity.” Commelin and Topaz supplied concrete examples as unit tests—objects that look and quack like ducks. These were not watertight evidence, but Commelin considered them at least as reassuring as reading conventional definitions.

11. Software verification is only as good as its target

• Scarfe raises Kim Morrison’s experiment using Claude agents to implement zlib in Lean. De Moura says the AI translated C code, repaired the implementation until it passed the C version’s test suite, and proved that, for any data and compression level, compressing then decompressing returns the original input.

• Scarfe’s pushback compares partial specifications to blind men examining different parts of an elephant. De Moura supplies the sharpest failure case: an identity function for both compression and decompression satisfies the round-trip property without compressing anything. Additional constraints might address output size and comparison with a Rust implementation’s compression on test cases.

• De Moura distinguishes assistance with a human examining the code from letting AI “go wild” without inspection. In the latter case, incomplete specifications can produce exactly the requested properties while missing the intended behavior. Hartnett also flags skepticism that specifications can adequately cover software at the complexity of most real programs.

• Scarfe calls review and verification the current bottleneck in agentic coding. Avigad suggests AI might help write specifications as well as implementations, increasing formal verification’s role, and notes that Harmonic believes mathematical-proving capabilities could transfer to software verification. Buzzard leaves the outcome open: “Whether or not it pans out, I don’t know.”

12. The infrastructure remains a human project

• Hartnett describes a decisive fracture during roughly 2018–2022, when de Moura withdrew to build Lean 4 while mathlib continued growing. He lacked a supporting engineering team and struggled with relentless user requests. Friction with Carneiro reflected different visions for Lean and its open-source mathematical library. De Moura’s complaint was that casually proposed ideas imposed increasingly expensive rebuttal work on their recipient.

• Hartnett reconstructed the story through six or seven core sources, private emails, and public and private Zulip conversations. Buzzard says trust developed when the participants recognized that Hartnett was not seeking villains or scandal. His own account ends with renewed friendship: an afternoon walking around Seattle with de Moura, talking about Lean and about life beyond it.

• Buzzard places himself at the excitement end of reactions ranging from “grief” to enthusiasm, while admitting nobody knows how good AI mathematics will become. He expects more theorems and understanding. He supplies the closing counterweight: “what makes our goals special is that they’re ours.” The relevant question remains how humans want to interact with machines and what they want to understand.