Claude formalizes Fermat's theorem in eleven days in Lean

On September 4, 2026, Anthropic announced that Claude had produced, in eleven days, the first complete machine-verified proof of Fermat's theorem in the Lean language: 13 million lines, roughly 29,500 intermediate theorems, a multi-agent platform (Prove2Me), and a review by Kevin Buzzard.

On September 4, 2026, Anthropic published a research post claiming that its Claude model produced the first end-to-end, machine-verified proof of Fermat's Last Theorem (FLT) in the Lean proof language. New Scientist relayed the announcement on September 5. According to Anthropic, the work took eleven days, generated 13 million lines of Lean, and proved 30,300 intermediate statements, of which 29,500 are part of the final proof.

The theorem states that there are no positive integers a, b, c such that aⁿ + bⁿ = cⁿ for an integer exponent n greater than 2. Formulated around 1637 by Pierre de Fermat, it was proved for humans only in 1995 by Andrew Wiles (with Richard Taylor filling a gap discovered after the 1993 announcement). What changes here is not a new "paper" demonstration, but an exhaustive translation of the argument into a form that a proof assistant can check line by line.

What a formalized Fermat's theorem from Claude means

Formalizing is not "asking a chatbot whether it believes Wiles is right." An assistant like Lean requires that every logical step be written in a formal language. Human proofs skip over the obvious steps; Lean skips none. They also rely on centuries of literature; a formalization can only rely on what is already in libraries like Mathlib, or on what is formalized along the way.

Anthropic insists on this point. Unlike recent work on the Riemann hypothesis, where the goal was to produce new mathematics, the novelty claimed for FLT is verification. Kevin Buzzard (Imperial College London), who until now led a multi-year project to formalize FLT, stated after review that the result "proves Fermat's theorem with no assumptions other than the axioms of mathematics," and that it shows autoformalization in algebra, harmonic analysis, geometry, and number theory.

According to Anthropic's post, the proof follows a simplified version of Wiles's argument presented by Henri Darmon, Fred Diamond, and Richard Taylor. It was verified by the Lean kernel using only the three standard axioms of Lean; a comparator confirmed that the statement matches the one in Mathlib. Anthropic also states that an independent verification was carried out with the Rust nanoda kernel (a detail picked up by several technical summaries).

How Prove2Me unlocked the Claude agents

The first multi-agent attempts failed in a way familiar to teams running long-running agents. After initial successes, the instances "lost track" of the project state and stopped collaborating effectively. Anthropic estimates that these failures nonetheless provided about 7% of the non-boilerplate lines of the final proof.

The turning point came with Prove2Me, an open platform designed by Tianyi Peng (Anthropic researcher, also affiliated with Columbia) and collaborators. According to Anthropic, Prove2Me served three concrete purposes. First, maintaining a directed acyclic graph (DAG) of statements to decide what to prove next and parallelize the work. Second, speeding up Lean compilation by separating statements and proofs. Third, facilitating search and reuse via natural-language descriptions of each theorem.

With Prove2Me and a multi-agent harness based on Claude Code, the team consumed about six billion output tokens of an internal research model judged "roughly comparable" to Claude Fable 5.1. Peng's human intervention, in the official account, is limited to high-level directives such as "Jacobian as a scheme sounds high priority" or "push [the] Mazur [theorem] to be done soon." The agents themselves flagged the moment the FLT root switched to the "PROVED" state (around August 17–18, 2026, according to the published excerpts).

The volume matters. At 13 million lines, the Lean proof would be five times larger than the current size of Mathlib, making it the largest Lean proof ever built — Anthropic nonetheless acknowledges that it is "probably much longer than necessary," with Mathlib remaining more compact and reviewed.

Who paved the way, and what the GitHub repository shows

The "eleven autonomous days" narrative must be read alongside its institutional context. Since 2024, Kevin Buzzard and the Lean community had been running an FLT formalization project at Imperial College London, with a blueprint of about sixty pages for the initial phase alone. Buzzard had already said, earlier in 2026, that AI progress would likely shorten the projected timeline (often cited at five years).

Several secondary analyses (including AI Weekly) point out that Anthropic's GitHub repository credits upstream files from the Imperial / Mathlib project — on the order of a hundred files according to these summaries — and presents the artifact as a research result (Apache 2.0, not maintained for external contributions). In other words, Claude did not reinvent the entire foundation from scratch; it massively accelerated an already charted formalization. Anthropic's post acknowledges this by citing the Imperial project, the flt-regular project, Lean, Mathlib, and the mathematical history (Frey, Serre, Ribet, Mazur, Langlands, etc.).

New Scientist also recalls that a conference bringing together AI experts and mathematicians had been organized in London around this endeavor. Anthropic's announcement "surpasses" it, in the sense that it closes, according to Buzzard, the goal of a machine-checked proof with no additional assumptions.

What formalization changes for mathematical research

Three consequences stand out from public statements.

First, the review burden. Verifying a groundbreaking proof can take months or years (Wiles in 1993–1995; Hales's Kepler conjecture; Perelman's Poincaré). If a Lean formalization accompanies a manuscript, part of the confidence becomes mechanical. Buzzard considers the autoformalization of FLT to be "a big step" toward the autoformalization of modern mathematical literature, to root out errors from the corpus and lighten the load on referees — and to audit LLM-generated mathematics, which is currently very costly to validate by hand.

Next, the pace. Anthropic describes a satellite experiment, with three personal Claude Max subscriptions, that formalized Vinogradov's three-primes theorem in three days via Prove2Me. The marketing message is clear: with the right scaffolding, major results become formalizable outside giant labs. Anthropic is also announcing credits and subscriptions for external researchers in pure mathematics and formalization.

Finally, the nuance. This is not an "elementary" proof of the kind Fermat might have written in the margin. Nor is it, according to Anthropic, a replacement for human exposition. The formalization complements a readable text; it does not make it superfluous. And the success depends as much on the multi-agent infrastructure (DAG, compilation, shared memory) as on the raw model. The initial failures demonstrate this.

For the general public using ChatGPT or Claude.ai, nothing changes on screen on September 5. For labs, journal editors, and teams betting on long-horizon agents, the signal is stronger. A legendary proof, awaited for years in Lean, has just been pushed through in less than two weeks of wall-clock time — at the cost of billions of tokens and careful orchestration.

Sources

• Anthropic, Formalizing Fermat's Last Theorem, September 4, 2026 — https://www.anthropic.com/research/formalizing-fermats-last-theorem
• New Scientist, Matthew Sparkes, Fermat's last theorem formalised by AI agents in just 11 days, September 5, 2026 — https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/
• Chen, Marwaha, Lu, Yuen & Peng, Prove2Me: An open collaborative platform for scaling math formalization, arXiv 2608.28433
• AI Weekly / technical summaries on Anthropic's GitHub repository and the Imperial / Mathlib credits

Frequently asked questions

What did Anthropic announce on September 4, 2026 about Fermat's theorem?

Anthropic announced that its Claude model had produced the first end-to-end, machine-verified proof of Fermat's theorem in the Lean proof language. The work took eleven days.

How large is the generated Lean proof?

The proof comprises 13 million lines of Lean and proves 30,300 intermediate statements, of which 29,500 are part of the final proof. At this size, it would be five times larger than the current size of Mathlib, making it the largest Lean proof ever built.

What does Fermat's theorem state?

The theorem states that there are no positive integers a, b, c such that aⁿ + bⁿ = cⁿ for an integer exponent n greater than 2. Formulated around 1637 by Pierre de Fermat, it was proved for humans in 1995 by Andrew Wiles, with Richard Taylor filling a gap.

What is Prove2Me and what was it used for?

Prove2Me is an open platform designed by Tianyi Peng and collaborators. It was used to maintain a directed acyclic graph of statements to parallelize the work, to speed up Lean compilation by separating statements and proofs, and to facilitate search and reuse via natural-language descriptions of the theorems.

How many tokens and which model were used for the proof?

The team consumed about six billion output tokens of an internal research model judged "roughly comparable" to Claude Fable 5.1, with a multi-agent harness based on Claude Code.

Did Claude build the formalization entirely from scratch?

No. Anthropic's GitHub repository credits upstream files from the Imperial College London project and Mathlib, on the order of a hundred files according to some summaries. Claude massively accelerated a formalization already charted since 2024 by Kevin Buzzard and the Lean community.

How was the proof verified?

The proof was verified by the Lean kernel using only Lean's three standard axioms, and a comparator confirmed that the statement matches the one in Mathlib. Anthropic also states that an independent verification was carried out with the Rust nanoda kernel.

What other result was formalized via Prove2Me?

Anthropic describes a satellite experiment, with three personal Claude Max subscriptions, that formalized Vinogradov's three-primes theorem in three days via Prove2Me.