Anthropic announced that its internal research version model, roughly equivalent to Claude Fable 5.1, completed a full formal proof of "Fermat's Last Theorem" in 11 days, generating a total of 13 million lines of Lean language code, making it the longest mathematical proof to date.

Fermat's Last Theorem was proposed by French mathematician Pierre de Fermat in 1637, stating that there are no positive integer solutions for aⁿ + bⁿ = cⁿ when n is greater than 2. This conjecture was first rigorously proven by British mathematician Andrew Wiles in 1995, with a paper spanning 129 pages.

Anthropic did not make new mathematical discoveries but rather "formalized" Wiles' original proof, rephrasing and verifying the entire proof chain using the Lean proof assistant language, which can be verified line by line by computers. During this process, 30,300 intermediate theorems were verified, with 29,500 ultimately included in the complete proof, consuming about 6 billion output tokens.

The project utilized a scheduling tool called "Prove2Me" to manage the dependencies between theorems in a directed acyclic graph structure, with dozens of Claude agents working in parallel. The statements of theorems were separated from the specific proof processes to enhance compilation efficiency. The project was led by Anthropic researcher Tianyi Peng (in collaboration with Columbia University) and built upon a formalization project initiated by mathematician Kevin Buzzard at Imperial College London. It also utilized the community-maintained mathematical formalization library Mathlib and the infrastructure of the non-profit Lean FRO, referencing 106 upstream files in GitHub submissions.

Buzzard confirmed after review that the proof "does not depend on any other assumptions besides the mathematical axioms themselves," and a comparison tool confirmed that the theorem statements in the proof matched the official versions in Mathlib. The complete proof has been uploaded to GitHub for independent verification, with Buzzard calling it a "historic moment (pending verification)."

The formalization work was completed between August 7 and 18, 2026, taking 11 days. The article also mentioned that the previous formalization project led by Buzzard at Imperial College has not yet been completed since its launch in 2024, with about 7% of the final generated code belonging to previously attempted failed or duplicated parts.

Source: Public Information