In just 11 days, Claude agents prepared the first fully computer-verified version of the proof for Fermat’s Last Theorem, as announced by Anthropic on September 4.
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.
Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of… pic.twitter.com/pdT8zwlV4A
— Anthropic (@AnthropicAI) September 4, 2026
Fermat’s Last Theorem states that the equation aⁿ + bⁿ = cⁿ has no solutions in positive integers a, b, and c for any integer n greater than two. Pierre de Fermat proposed this theorem in 1637.
The result pertains to the formalization of the known proof published by Andrew Wiles in 1995. Claude translated the mathematical reasoning into code that the proof verification system Lean can verify step by step.
How Claude Agents Worked
The experiment was organized by Anthropic researcher Tianyi Peng, whose team at Columbia University develops tools for the formalization of mathematics. According to a technical report, humans provided the formulation of the target theorem and occasionally set priorities.
The agents independently recorded intermediate statements, verified each other’s formulations, and constructed proofs.
The system utilized the Mathlib library and materials from the Imperial College London FLT and flt-regular projects. In the final code, 106 files were adapted from these projects with authorship noted.
The Prove2Me platform helped coordinate the agents. An article by its developers describes the collaborative work principle: a large task is broken into related intermediate statements, and participants add proofs and use existing results. The overall structure allows multiple agents to work in parallel.
According to Anthropic, Claude proved about 30,300 intermediate theorems, with approximately 29,500 included in the final work. The code volume reached 13 million lines.
The company described the result as the largest proof on Lean, noting that the code is likely significantly longer than necessary.
The experiment used an internal research model, roughly comparable to Claude Fable 5.1. The work required about 6 billion output tokens.
How the Result Was Verified
The complete code and instructions for re-verification are published on GitHub. According to the documentation, the proof passed verification by Lean and the independent checking core nanoda. The comparator tool confirmed the final statement’s alignment with Fermat’s theorem as formulated in Mathlib.
The authors also established that the proof uses only three standard Lean axioms and contains no unproven placeholders. The repository notes that the reliability of the result assumes trust in the verifying programs.
Kevin Buzzard, a mathematician from Imperial College London who is conducting his own theorem formalization project, separately confirmed the result in his blog.
“I compiled the codebase and ran the comparator on it — the check passed,” he wrote.
Buzzard linked the significance of the work to the potential of automatic formalization. In his view, such tools can help verify scientific papers and identify gaps in reasoning.
The researcher will continue his own project. In addition to formalization, his tasks include enriching Mathlib and creating a document that allows people to study the modern version of the proof. Claude worked with an exposition of an earlier approach.
In July, Claude Mythos Preview assisted Anthropic researchers in finding cryptanalytic attacks on the post-quantum signature scheme HAWK and a shortened seven-round version of AES-128. The result for AES did not pertain to the full ten-round version of the cipher.
