In an impressive feat, Claude agents have developed the first fully computer-verified proof of Fermat's Last Theorem in just 11 days, as announced by Anthropic on September 4.
Verifying a significant mathematical proof can take years. The process of formalization—translating mathematical reasoning into a format that computer proof assistants like Lean can validate—can expedite this.
Last month, Claude achieved the first formalized proof of Fermat’s Last Theorem, one of… pic.twitter.com/pdT8zwlV4A
— Anthropic (@AnthropicAI) September 4, 2026
Fermat's Last Theorem posits that the equation aⁿ + bⁿ = cⁿ has no solutions in positive integers a, b, and c when n is an integer greater than two. Pierre de Fermat first stated this conjecture in 1637.
This recent accomplishment involves the formalization of an already established proof published by Andrew Wiles in 1995. Claude translated the mathematical arguments into code that the Lean proof-checking system can verify step by step.
How Claude Agents Operated
The experiment was led by Anthropic researcher Tianyi Peng, whose team at Columbia University is focused on developing tools for formalizing mathematics. According to a technical report, human contributors provided the formulation of the theorem and occasionally set priorities.
The agents autonomously recorded intermediate statements, checked each other's formulations, and constructed the proofs.
The system utilized the Mathlib library along with resources from the Imperial College London projects FLT and flt-regular. The final code comprises 106 files adapted from the two latter projects, with proper attribution.
Coordination among agents was facilitated by the Prove2Me platform. In a paper by its developers, the collaborative approach is outlined: the large task is divided into interrelated intermediate statements, with participants contributing proofs and leveraging previously established results. This structure allows multiple agents to work simultaneously.
According to Anthropic, Claude proved approximately 30,300 intermediate theorems, of which about 29,500 were included in the final output. The total code volume reached 13 million lines.
The company referred to this outcome as the largest proof in Lean, noting that the code is likely much longer than necessary.
The experiment employed an internal research model roughly comparable to Claude Fable 5.1. It generated around 6 billion output tokens.
Verification of the Result
The complete code and instructions for replication are available on GitHub. According to the documentation, the proof has passed validation by Lean and an independent verifier known as nanoda. The comparator tool confirmed that the final statement aligns with Fermat's theorem as defined in Mathlib.
The authors also established that the proof relies solely on three standard axioms of Lean and does not contain any unproven placeholders. The repository specifies that the reliability of the result assumes trust in the verification programs used.
Kevin Buzzard, a mathematician at Imperial College London who is pursuing his own formalization project of the theorem, separately confirmed the result on his blog.
"I compiled the codebase and ran the comparator — the verification was successful," he stated.
Buzzard linked the significance of this work to the capabilities of automated formalization tools, suggesting that such instruments could aid in reviewing scientific papers and identifying gaps in reasoning.
He plans to continue his own project, which will not only focus on formalization but also on enhancing Mathlib and creating documentation to help individuals learn the modern version of the proof. Claude's work was based on an earlier approach to the theorem.
It is worth noting that in July, Claude Mythos Preview assisted Anthropic researchers in uncovering cryptanalytic attacks on the post-quantum signature scheme HAWK and a reduced semi-round version of AES-128. The AES result did not pertain to the complete ten-round version of the cipher.