Claude Formalizes Fermat’s Last Theorem in Lean in 11 Days

Anthropic announced on September 4 that Claude had produced the first complete computer-checked proof of Fermat’s Last Theorem. According to the company, dozens of Claude agents worked largely autonomously for 11 days, generated approximately 13 million lines of Lean code, and proved 30,300 theorems, of which about 29,500 appear in the final proof.

This is not a new proof of Fermat’s Last Theorem in the conventional mathematical sense. Andrew Wiles and Richard Taylor completed the accepted human proof in the 1990s. Claude instead translated an established route through the literature into a formal language whose logical steps can be checked by a computer.

The distinction matters. The result adds essentially no new knowledge about whether Fermat’s Last Theorem is true, but it demonstrates that an AI system can formalize a body of advanced mathematics previously expected to require years of specialist work. Kevin Buzzard, the Imperial College London mathematician leading a separate formalization project, compiled Anthropic’s code and ran its comparator checks. He reported that the proof checks out.

1. What Claude Formally Proved

Fermat’s Last Theorem states that no positive integers \(a\), \(b\), and \(c\) satisfy \(a^n+b^n=c^n\) when the integer exponent \(n\) is at least three. The statement is elementary, but its known proofs depend on sophisticated results involving elliptic curves, modular forms, Galois representations, deformation theory, algebraic geometry, and number theory.

Anthropic’s repository expresses the final theorem directly over Lean’s natural numbers. Its statement takes positive natural numbers \(a\), \(b\), and \(c\), together with \(n \geq 3\), and proves that the equation cannot hold. A separate final check derives Mathlib’s existing statement of Fermat’s Last Theorem from this theorem.

The argument follows the work of Frey, Serre, Ribet, Wiles, and Taylor–Wiles, particularly the 1995 exposition by Henri Darmon, Fred Diamond, and Richard Taylor. It uses the connection between a hypothetical solution to Fermat’s equation and a Frey elliptic curve, then applies modularity and level-lowering results to obtain a contradiction.

Buzzard identified an important detail in the construction. Anthropic’s Wiles-based path handles prime exponents \(p \geq 17\). The complete result incorporates previously formalized work on regular primes to close the remaining cases. The resulting Lean theorem nevertheless covers every natural-number exponent of at least three.

The artifact also depends on substantial earlier human work. Anthropic says it adapted material from the Imperial College FLT project, the flt-regular project, and Mathlib. Its attribution file identifies 106 files containing material from the first two projects and 23 files that reproduce Mathlib text. The achievement is therefore an AI-led integration and expansion of an existing formal ecosystem, not 13 million lines created independently of prior formal mathematics.

2. How a Multi-Agent System Managed the Proof

Anthropic initially found that Claude agents could prove individual results but lost track of the wider project. Agents duplicated work, failed to reuse completed theorems effectively, and stopped coordinating as the proof grew. Failed attempts still account for about 7% of the final non-boilerplate code.

The successful run used Prove2Me, an open collaborative formalization platform developed by Tianyi Peng and collaborators at Columbia University. Prove2Me represents a project as a directed acyclic graph of theorem statements. Agents can select unfinished nodes, prove prerequisites, and reuse results produced elsewhere in the graph.

The platform also separates theorem statements from their proofs. That design reduces recompilation costs and lets the system change or replace a proof without disrupting every dependent statement. Natural-language descriptions attached to theorem nodes give agents another way to search the growing library and identify useful dependencies.

A Claude Code-based multi-agent harness coordinated dozens of agents over the 11-day run. Human mathematical input was reportedly limited to occasional high-level priorities, such as directing the agents toward Jacobians or asking them to complete a theorem associated with Mazur’s work. An internal log recorded the root theorem as proved on August 18.

Anthropic reports that the run consumed roughly six billion output tokens. It used an internal general-purpose research model described only as approximately comparable to Claude Fable 5.1, so the exact model and configuration are not publicly available. The company has not disclosed the project’s monetary or compute cost.

The finished development contains 29,511 theorem pages and 1,450 definition modules in its browsable documentation. Anthropic counts 30,300 computer-verifiable theorems across the wider run, including results that were not ultimately needed by the final dependency path.

3. How the Proof Was Checked

A formal proof is valuable only if the theorem statement, permitted assumptions, and verification process are controlled. Anthropic’s repository pins the project to Lean 4.33.1 and Mathlib 4.33.0 and includes several layers of checking.

First, the project was built from scratch. Its 60,475 modules were checked by the Lean kernel. The final theorem depends on exactly three standard Lean axioms: propositional extensionality, classical choice, and quotient soundness. The distributed proof modules contain no unfinished sorry placeholders, newly declared axioms, unsafe code, native decision shortcuts, or external implementations.

Second, the project used the Lean Comparator to compare the proved theorem against a separately supplied challenge statement based only on Mathlib. This check is designed to establish that the solution proves the same proposition, uses no unapproved axioms, and is accepted by the kernel. The comparator returned its acceptance verdict.

Third, an independent Lean kernel implementation called nanoda checked an exported version of the environment and accepted 1,052,234 declarations without errors. Anthropic applied four patches to nanoda: one for progress output and three to accelerate definitional-equality searches. The repository says none changes or weakens a typing rule.

Buzzard supplied the most relevant external confirmation. He compiled the code on a 96-core machine and ran the comparator himself. He described the repository as more than 13.4 million lines and said it took nearly 20 times as long to compile as Lean’s mathematics library.

Reproducing every check is possible but hardware-intensive. Anthropic’s documented build took 5 hours and 32 minutes at 96 parallel jobs, peaked at 153 GB of memory, and used approximately 67 GB for the Lean build plus as much as 220 GB of removable generated C files. Its comparator run took 14 hours and 46 minutes and peaked at 230 GB. Exporting the environment for the second kernel produced a 37.8 GB file.

These checks establish that the exact formal statement follows from the listed axioms, assuming the correctness of at least one checking kernel and the surrounding verification tools. They do not automatically establish that every intermediate theorem’s machine-generated name accurately describes its mathematical meaning. Anthropic addresses that limitation with a proof-path document mapping the major mathematical steps to their exact Lean statements.

4. What Changed for AI-Assisted Mathematics

Before this result, Fermat’s Last Theorem was the remaining entry in Freek Wiedijk’s long-running list of 100 notable theorem-formalization challenges. The Imperial College project began in 2024 with five years of funding and initially aimed to reduce the theorem to results known by the end of the 1980s. Its project materials noted that a complete formalization would require translating thousands of pages of informal mathematics.

Anthropic’s proof instead reaches the final theorem end to end. Buzzard emphasized that this does not make his project redundant: the Imperial effort is developing reusable, human-readable additions to Mathlib and follows a more modern proof. Anthropic labels its repository a research artifact that will not be maintained and is not accepting contributions.

The practical advance is therefore in throughput. Claude’s agents assembled formal definitions and proofs across algebra, harmonic analysis, geometry, and number theory on a scale that exceeded Mathlib’s line count by more than five times. The result shows that a graph-based agent system can preserve dependencies and coordinate work across a formalization too large for a single model context.

The proof also demonstrates a verification path for AI-generated mathematics. A language model can produce an incorrect natural-language argument with convincing prose, but Lean rejects a proof term that does not type-check. A separately controlled theorem statement and comparator further reduce the risk that an agent succeeds by quietly weakening or changing the problem.

That mechanism does not remove the need for mathematicians. Humans must still decide whether a formal statement captures the intended concept, assess the importance and exposition of a result, and maintain reusable libraries. It can, however, move exhaustive checking of logical steps from human referees to proof-assistant kernels—provided the definitions, theorem statement, and trusted verification boundary are independently inspected.

Frequently Asked Questions

Did Claude discover a new proof of Fermat’s Last Theorem?

No. It formalized an established route through the Frey–Serre–Ribet–Wiles–Taylor–Wiles literature so that Lean could check every logical step.

Was the result independently verified?

Kevin Buzzard compiled the public code and ran the Lean Comparator, reporting that it checks out. The repository also records successful checks by Lean and the independent nanoda kernel.

Which Claude model produced the proof?

Anthropic has not named an exact public model. It describes the internal general-purpose research model as roughly comparable to Claude Fable 5.1.

Can researchers reproduce the verification?

Yes, the code and instructions are public under the Apache 2.0 license. Full reproduction requires substantial hardware, including hundreds of gigabytes of memory for some verification stages.

Is the 13-million-line repository entirely new AI-written mathematics?

No. The AI agents generated and integrated most of the development while building on Mathlib and earlier open-source formalization work from the Imperial College FLT and flt-regular projects.

Sources

• Original Anthropic announcement on X
• Anthropic: Formalizing Fermat’s Last Theorem
• Anthropic’s Fermat’s Last Theorem repository
• Kevin Buzzard: FLT—Anthropic Has Beaten Me to It
• Prove2Me research paper
• Imperial College London’s Lean formalization project
• Lean Comparator repository and verification model