What happened
Anthropic says Claude worked largely autonomously for 11 days to produce an end-to-end, computer-checked formalization of Fermat’s Last Theorem in the Lean proof assistant. The company says the proof was checked by Lean, used only Lean’s three standard axioms, and was reviewed by mathematician Kevin Buzzard.
Anthropic reports that Claude formalized Fermat’s Last Theorem, the statement that no positive integers satisfy aⁿ + bⁿ = cⁿ for n greater than 2. The theorem was first proved by Andrew Wiles in 1995. Anthropic emphasizes that the new work formalizes and verifies an existing mathematical result rather than discovering a new proof.
According to Anthropic, Claude generated 13 million lines of Lean code, proved 30,300 intermediate theorems, and used 29,500 of them in the final proof. Dozens of Claude agents collaborated through Prove2Me, an open platform that tracked dependencies between theorem statements and helped agents work in parallel.
Anthropic says the finished proof was checked by Lean and uses only Lean’s three standard axioms. The company also says a comparator confirmed that the theorem statement matched Mathlib’s statement of Fermat’s Last Theorem. Kevin Buzzard reviewed the proof and described the achievement as significant, while Anthropic notes that the result remains subject to re-checking.
The company says early attempts failed because agents lost track of the project’s state. The effort succeeded after the researchers adopted Prove2Me and a Claude Code-based multi-agent harness. Anthropic estimates that the project consumed about six billion output tokens from an internal research model roughly comparable to Claude Fable 5.1. The source does not provide a public price for reproducing the full effort or establish that the same result is currently practical for ordinary Claude users.
Source details: anthropic.com ↗
Why it matters
The work addresses verification rather than discovering a new proof of Fermat’s Last Theorem. If independently reproduced, it would show that AI systems can help translate extremely complex human mathematics into machine-checkable form, potentially reducing the time required to verify future proofs and AI-generated mathematical claims. The result also highlights that useful autonomy may depend as much on project-management tools and formal scaffolding as on the underlying model.
Formal proof assistants such as Lean check whether each logical step follows from prior definitions, theorems, and axioms. That can provide a stronger correctness check than ordinary peer review, although it does not by itself make a proof understandable to non-specialists or establish that the formalized statement captures every intended mathematical nuance.
The claimed advance is in scale and speed. Anthropic says the formalization was expected to take years based on the community’s existing blueprint, while Claude completed it in 11 days. If the public code survives independent scrutiny, the approach could help mathematicians check long proofs and inspect AI-generated mathematics more efficiently.
The result is also a systems demonstration. Anthropic attributes success not only to Claude but to dependency tracking, theorem search, parallel collaboration, faster compilation, and a multi-agent workflow. That suggests future mathematical automation may depend on specialized infrastructure rather than on a model operating alone.
Important limitations remain. The source is Anthropic’s own account of its system, and the article does not report a completed independent audit, external replication, comparative costs, or a peer-reviewed assessment of the entire artifact. Buzzard’s review is meaningful evidence of expert engagement, but it is not equivalent to broad independent validation.
What to watch next
Independent mathematicians’ re-checking of the publicly available Lean code will be important, as will evidence that the approach generalizes beyond a theorem with an existing proof blueprint. The practical cost, reproducibility on external systems, and usability of the resulting proof for human mathematicians remain unclear.
Watch for independent checks of the GitHub proof, including whether it compiles from the published materials and whether outside Lean users identify errors, hidden assumptions, or dependencies not described in the announcement.
Watch whether the same workflow can formalize other major theorems without an unusually detailed human-developed blueprint. Anthropic reports a smaller experiment formalizing Vinogradov’s Three Primes Theorem in three days using three personal Claude Max plans, but the source gives no independent evaluation of that result.
The cost and access model are unresolved. Anthropic says it offers free or discounted subscriptions, research credits, and dedicated grants for larger projects, but it does not state that the full Fermat formalization can be reproduced through a consumer subscription or disclose the monetary cost of the reported six billion output tokens.
The broader test will be whether formalization becomes a routine companion to human-readable mathematical papers. Anthropic argues that machine-checkable proofs could help referees keep pace with AI-generated work, while also acknowledging that formalized proofs should not replace explanations written for human readers.