Claude’s Fermat Formalization Tests AI on Research a Computer Can Verify

Anthropic says Claude helped produce the first complete computer-checked formal proof of Fermat’s Last Theorem in Lean. The 11-day workflow generated roughly 13 million lines of code and relied on dozens of agents, a coordination system called Prove2Me, and machine verification rather than human trust in the model’s reasoning.¹

The central caveat is also why the result matters: Claude did not discover a new proof of Fermat’s Last Theorem. It formalized an existing proof route, drawing on decades of mathematics, Lean’s Mathlib library, and prior human formalization work.¹²⁷ In AI research terms, the stronger claim is not that a model solved Fermat. It is that an AI-agent workflow produced a massive artifact whose final correctness can be checked by proof-assistant software.

That makes formal mathematics an unusually clean proving ground for AI reliability research. In many long-horizon tasks, success is judged by human evaluation, benchmarks, or downstream usefulness. In Lean, a proof either type-checks against a stated theorem and permitted axioms, or it does not. The model can generate candidate code, but the Lean kernel is the gatekeeper.⁶

What Anthropic says Claude produced

According to Anthropic, the project began as researcher Tianyi Peng’s attempt to test whether Claude could make progress on formalizing Fermat’s Last Theorem. The run produced an end-to-end Lean proof after 11 days of largely autonomous work. During that period, Claude wrote about 13 million lines of Lean and proved 30,300 intermediate theorems, about 29,500 of which were used in the final proof.¹

The proof follows a simplified version of the Wiles-era route through an exposition by Henri Darmon, Fred Diamond and Richard Taylor, rather than introducing a new mathematical argument.¹² Fermat’s Last Theorem states that no positive integers a, b and c satisfy aⁿ + bⁿ = cⁿ for integer n greater than 2. Andrew Wiles, with Richard Taylor’s contribution to repairing a gap, established the theorem in the 1990s. The Anthropic work translates that human mathematics into a machine-checkable form.¹⁷

The company says the final proof was checked by Lean, used only Lean’s standard axioms, and was compared against Mathlib’s statement of Fermat’s Last Theorem to ensure the formal theorem matched the intended target.¹⁴ AI Stack Current reports additional verification boundaries around the release, including checks for omitted-proof shortcuts, comparator validation, and verification by an independent Lean kernel implementation, nanoda.⁶

What was automated — and what was not

The automated work was substantial but scaffolded. Anthropic describes a multi-agent workflow in which Claude agents defined concepts, proved intermediate lemmas, and assembled dependencies toward higher-level theorems.¹ Coverage from SiliconANGLE and Techstrong.ai says several dozen agents worked in parallel and generated roughly 6 billion output tokens.³⁴

The successful run depended on Prove2Me, an open collaborative formalization platform built by Peng and collaborators at Columbia University. Anthropic says early attempts failed because agents made initial progress but lost track of the project’s state and stopped cooperating effectively. Prove2Me supplied an external dependency graph, tracked theorem statements, separated statements from proofs to reduce compilation overhead, and helped agents search for and reuse prior results.¹

That distinction matters for engineering readers. The result was not a single model sitting in one uninterrupted context window and proving a theorem from scratch. It was a distributed agent system with persistent external state, explicit decomposition, reuse of completed lemmas, and deterministic compilation checks.⁴⁸

Human input also remained part of the process. Anthropic says human mathematical direction was limited to occasional high-level guidance from Peng, such as prioritizing certain mathematical objects or theorems.¹ Kevin Buzzard, a leading Lean formalization researcher at Imperial College London, reviewed the proof and supplied comments quoted by Anthropic.¹ Buzzard, author of the Xena Project, also says he compiled the code base and ran a comparator on it, concluding that it checked out.²

The main scrutiny points

The first scrutiny point is attribution. AI Weekly notes that Anthropic’s repository credits upstream work from Imperial College London’s FLT project, Mathlib, and related formalization efforts, complicating any simple narrative that the result was autonomous or clean-room.⁵ Anthropic itself acknowledges that the proof adapts pieces from the Imperial College London FLT project, the flt-regular project, Mathlib, and earlier mathematical literature.¹

The second is novelty. The Xena Project reaction is blunt: mathematically, the formalization adds little to the community’s confidence that Fermat’s Last Theorem is true, because the theorem was already accepted. Its significance is in autoformalization capability.² DiarioBitcoin makes the same distinction for a broader audience, stressing that Claude formalized a known proof route on top of years of human-built infrastructure rather than discovering a new proof.⁷

The third is maintainability. A 13-million-line proof is an engineering achievement, but it is also large, expensive to compile, and likely far longer than an optimized human-curated formalization would be. Anthropic notes that the artifact is more than five times the size of Mathlib and likely longer than necessary.¹ AI Stack Current reports that verification required significant compute and memory, underscoring that machine-checkable does not automatically mean lightweight or easy to audit.⁶

The fourth is the boundary of the trusted system. A Lean proof reduces reliance on model judgment, but it does not eliminate every assumption. Reviewers still need to trust the proof kernel, the formal statement, the build environment, the absence of disallowed shortcuts, and the match between the formal theorem and the informal theorem mathematicians care about.⁶

Why proof assistants are attractive for AI reliability

For AI researchers, the story is less about Fermat’s Last Theorem as a trophy and more about the evaluation loop. Formal mathematics gives AI agents a rare target: long-horizon work with exact pass-fail checks at every stage. The model can be creative, messy, and verbose, but the proof assistant rejects invalid steps.

That architecture resembles a broader reliability pattern: use generative models to search a large space of candidate solutions, then use independent verifiers to decide what counts. In software, that verifier might be a compiler, test suite, model checker, or static analyzer. In formal mathematics, it is a proof kernel operating over definitions, axioms, and previously verified theorems.⁶

That is why the 11-day workflow matters even though the theorem was not newly discovered. It suggests AI agents may become more useful in domains where output can be reduced to a formal artifact and checked outside the model. Guozhen AI framed the next question as whether the pipeline can be reused for other major theorems and for reliability-critical verification in software and safety work.⁸

What comes next

The near-term benchmark is replication and reuse. Other researchers can inspect the released repository, rebuild the proof, test the comparator setup, and evaluate which parts of the artifact are new, adapted, or mechanically ported.⁶ The Xena Project reaction suggests the result may accelerate, rather than replace, human-led formalization work aimed at producing maintainable libraries and explanatory documents for mathematicians.²

The longer-term question is whether formalization becomes a normal companion to AI-generated research. Anthropic argues that proof assistants could reduce the burden on referees and help check AI-generated mathematics before humans invest months or years evaluating it.¹ That is plausible in fields where definitions can be formalized and proof obligations can be decomposed. It is less clear in empirical science, policy analysis, or open-ended engineering design, where the verifier is incomplete or contested.

For now, Claude’s Fermat formalization is best read as a major autoformalization milestone, not a declaration that AI can autonomously do arbitrary research. Its importance comes from the constraint that made the headline possible: the final answer was not accepted because Claude sounded convincing, but because a proof assistant could check the work line by line.

Claude’s Fermat Formalization Tests AI on Research a Computer Can Verify

More from Siften Technology

OpenAI’s Navier–Stokes Claim Shifts Focus to Verification

Things to know

Comments

Source Material

What Anthropic says Claude produced

What was automated — and what was not

The main scrutiny points

Why proof assistants are attractive for AI reliability

What comes next

Key topics covered

At IFA Berlin, AI Robots Leave the Stage—but Not Yet for Everyday Life

Elementor Pro flaw exposes WordPress sites to mass exploitation

GitHub’s GPT-6 Astra rollout makes AI model choice an enterprise control layer