Autoformalization is the use of AI systems to translate mathematical arguments written for human readers into the formal language of a proof assistant — in current practice almost always Lean 4 — so that a small trusted kernel can verify every inferential step mechanically. It is distinguished from AI systems that produce new mathematics: the object of an autoformalization effort is a proof that already exists, and the contribution is certification rather than discovery. The distinction is stated in those terms by the two principal 2026 artifacts, and is the load-bearing qualification when reading claims about either.
The practical significance is that formal verification is the one check on machine-generated mathematics that does not scale with human reviewer time. As AI systems produce more purported proofs than referees can evaluate, formalization offers a certificate whose cost falls with model capability rather than rising with output volume.
The verification problem it addresses
The motivating observation is that confidence in a long mathematical argument is expensive and slow to obtain. Andrew Wiles presented a proof of Fermat's Last Theorem in June 1993; two months into verification a reviewer exposed a gap that took a year to repair, and the corrected proof was published in May 1995 (Formalizing Fermat's Last Theorem (Anthropic, September 2026)). Comparable cases recur: Thomas Hales's 1998 Kepler conjecture proof spent four years in review before a twelve-referee panel settled for "99% certain," and was later formalized through the twenty-person Flyspeck project; Grigori Perelman's 2002 Poincaré conjecture proof took roughly four years and three 300-page expositions to be accepted; Harald Helfgott's 2013 weak Goldbach proof remains under review (Formalizing Fermat's Last Theorem (Anthropic, September 2026)).
Formalization was the proposed remedy long before AI made it tractable at scale. The Dutch computer scientist Jan Bergstra proposed formalizing Wiles's proof around 2005, and Kevin Buzzard began a multi-year community effort in Lean at Imperial College London in 2024; the blueprint for that project's initial phase alone runs to 86 pages, and the effort was funded for five years (Formalizing Fermat's Last Theorem (Anthropic, September 2026); Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)).
Barriers before agents
Three obstacles are named consistently in the literature (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)):
- Expertise. Writing formal proofs requires simultaneous command of the mathematics and of proof-assistant engineering, confining the work to a small community. Peter Scholze's Liquid Tensor Experiment required roughly eighteen months of sustained community effort.
- Reusability. Formalizations are released as monolithic Git repositories of tightly interdependent theorems. Because Lean recompiles the entire downstream cone when a module changes — even for a proof-only edit — integration serializes through a merge queue, and individual results are hard to extract for use elsewhere.
- Compute concentration. Large agent swarms run on a single organization's internal infrastructure, with tens of thousands of agents and five-figure per-project budgets, leaving contributions from anyone outside untapped.
The audit gap
A proof assistant's kernel certifies that a proof inhabits a stated theorem. It does not certify that the stated theorem is the one intended. An AI-generated statement "can be vacuous, miss a hypothesis, or drift semantically, yet still be 'proved'" — and a Lean-as-judge audit reported by Bourigault et al. (2026) found only about 43 percent of proved statements faithful to their intended claims (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)).
The mitigation now standard across projects is to shrink the human audit surface rather than to expand it: reviewers check definitions and top-level statements, not proofs. Prove2Me fixes that surface in advance through audited missions, in which a mission's goal statement, the definitions it rests on, and its milestone lemmas are human-reviewed while agents introduce the remaining intermediate theorems freely (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)). An independent check of the same kind was applied to the Fermat's Last Theorem result: a comparator tool confirmed that the formalized theorem statement matches Mathlib's own statement of the theorem, and the proof uses only Lean's three standard axioms (Formalizing Fermat's Last Theorem (Anthropic, September 2026)).
Decomposition as the enabling mechanism
The technical move that made project-scale multi-agent formalization work is the separation of a theorem's statement from its proofs, with each statement an immutable, independently compilable object. A proof-sketch may then import other platform theorems, including ones not yet proved, establishing its target conditional on them; by the Curry–Howard correspondence, importing a theorem is equivalent to assuming a term of that type. Because statements are immutable, a sorry-free proof-sketch is a permanent guarantee, and each imported child lemma becomes an atomized problem an agent can attack without compiling the parent (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)).
The alternative — asking agents to fill sorry placeholders in shared files — fails for two reasons the same paper states: recompilation cost, and the interference of concurrent edits to the same files, which prevents clean partitioning of the work. Git workflows resolve the second at the cost of centralizing review in human maintainers or an orchestrating agent.
Two coordination failures remain even with decomposition, and milestones address them: independent agents formalizing the same lemma in mutually incompatible ways, so that parallel effort duplicates rather than accumulates, and a formalization that silently deviates from the source contaminating every proof-sketch that imports it (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)).
Reported results, 2026
| Project | Object | Scale | Resources reported |
|---|---|---|---|
| Fermat's Last Theorem (Anthropic, Sept 2026) | Wiles's 1995 proof, via the Darmon–Diamond–Taylor exposition | 13M lines of Lean; 30,300 theorems proved, 29,500 used | 11 days; ~6 billion output tokens; an internal research model Anthropic calls roughly comparable to Claude Fable 5.1 |
| Vinogradov's Three Primes Theorem (Anthropic, 2026) | Existing theorem | not stated | 3 days; three personal Claude Max subscriptions |
| Bandit Algorithms (Prove2Me) | Lattimore and Szepesvári textbook | 151K lines | 13 days; 6 agents; ~$400 on consumer subscriptions |
| Exact Matrix Completion (Prove2Me) | Candès and Recht (2009) paper | 81K lines | 16 days; 9 agents; ~$600 |
| Algebraic Combinatorics (Gloeckle et al., centralized swarm) | Textbook | 130K lines | 7 days; 30,000 agents; ~$100,000 metered API inference |
Sources: Formalizing Fermat's Last Theorem (Anthropic, September 2026), Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026). The cost figures are not on a common basis — the centralized swarm's is metered API inference, the Prove2Me rows are flat-rate consumer subscriptions priced at roughly $200 per month per human contributor — and the Prove2Me authors state explicitly that their table "reports case studies, not a controlled experiment," since corpora, difficulty, working patterns and model generations differ across rows. They also name the confound their own comparison cannot resolve: a stronger model generation and a harness built for multi-agent proving are not separated by these data.
A separate use of formalization appears alongside AI-produced new results rather than as certification of old ones. OpenAI's August 1, 2026 publication of ten mathematics and theoretical-computer-science results released Lean formalizations for the arguments (Ten Advances in Mathematics and Theoretical Computer Science), and Anthropic's August 2026 Riemann zeta-function result was accompanied by a Lean formalization produced by Eric Easley (Source: anthropic.com). In this posture the formal certificate answers a narrower question — whether the argument is valid — while leaving the selection, novelty and significance questions that OpenAI's amazing — but vastly oversold — new model Astra (Marcus, August 2026) and Ernie Davis raise about such publications untouched.
What formalization does and does not settle
Practitioners on both sides of the AI-mathematics debate treat the certificate as narrow. Kevin Buzzard, reviewing the Fermat's Last Theorem formalization, stated that it "proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics" and that "AI autoformalization artefacts are now robust enough to be built upon," and drew the forward inference that such techniques "will enable us to rigorously check LLM-generated mathematics, which is currently typically an extremely costly human-led process" (Formalizing Fermat's Last Theorem (Anthropic, September 2026)).
The Prove2Me authors state the limit from the other direction: the platform's "vision is not to replace mathematicians," since "[c]hoosing what is worth formalizing, decomposing it into milestones, and judging whether a formal statement says what it is meant to say all remain matters of human judgment; agents supply the mechanical labor beneath those decisions." Agents on the platform are required to write a natural-language account of every statement and proof they submit, so that output remains legible to people (Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)). Anthropic states the same boundary — that a formalized proof "should not replace a human-understandable exposition" — while expecting it to become common to publish one alongside any write-up intended for human readers (Formalizing Fermat's Last Theorem (Anthropic, September 2026)).
A reported side effect runs in the other direction, from formalization back to capability: Anthropic states that writing Lean "seems to help Claude prove novel results," with recent model-authored results formalized in parallel with their proofs and the partial formalizations used by the model to check its own hypotheses (Formalizing Fermat's Last Theorem (Anthropic, September 2026)). The claim is stated without supporting measurement.
Open questions
- Whether a formalized corpus can be searched effectively as it grows. The Prove2Me authors name locating the right existing theorem to import as the central efficiency problem for a large, evolving library of formal statements.
- How decentralized, asynchronous agents exchange harnesses, lessons and context — the coordination problem the authors distinguish from the centralized-orchestrator setting that most multi-agent research assumes.
- How an open submission platform rejects adversarial or low-quality contributions, and whether a reputation system suffices.
- How human-legible insight is extracted from machine-generated proofs measured in millions of lines. Anthropic notes that its own proof is "likely much longer than it needs to be" relative to the concise, well-reviewed Mathlib.
- Whether the harness or the model generation accounts for the reported efficiency gains, which no published comparison isolates.
Relationships
- depends-on: Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)
- depends-on: Formalizing Fermat's Last Theorem (Anthropic, September 2026)
- instance-of: AI for Science
- related: Ten Advances in Mathematics and Theoretical Computer Science
- related: Verification Asymmetry
- related: Agentic AI
- related: Agent Architecture Patterns
- related: Anthropic
- related: OpenAI
- related: Claude Fable 5.1
- related: Machine-produced mathematics: claims, verification and credit — the 2026 machine-produced mathematical claims compared on what formalization does and does not settle