Anthropic said its Claude model produced the first complete computer-checked proof of Fermat’s Last Theorem in 11 days by writing the proof in the Lean programming language.. The company said Claude worked largely autonomously, generated 13 million lines of Lean code, and proved 30,300 theorems during the effort, with 29,500 used in the final proof..
Fermat’s Last Theorem states that no positive integers a, b and c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2. The theorem remained unproven for more than 350 years until Andrew Wiles published the first accepted proof in 1995.. Anthropic researcher Tianyi Peng began the project to test whether Claude could make progress on formalizing the theorem.
The formalization effort had been expected to take years, and the mathematical community had been using an 86-page blueprint for the initial phase of the work.. Claude’s proof follows a simplified version of Wiles’s proof from Darmon, Diamond and Taylor. Anthropic said human input was limited to occasional high-level instructions from Peng, including prompts such as “Jacobian as a scheme sounds high priority” and “push Mazur theorem to be done soon.”.
Kevin Buzzard of Imperial College London, who launched a community effort in 2024 to formalize the theorem in Lean, called the result “an extraordinary autoformalization achievement.” He said the work showed autoformalization across algebra, harmonic analysis, geometry and number theory.. Anthropic said early attempts by Claude failed because agents lost track of the project’s state and stopped collaborating effectively.
Those failed efforts accounted for about 7% of the non-boilerplate lines in the final proof.. The company said the effort succeeded after switching to Prove2Me, an open collaborative platform for formalizing mathematics designed by Peng and collaborators at Columbia University. With Prove2Me and a Claude Code-based multi-agent system, the proof was completed in a little under two weeks using about six billion output tokens from an internal research model roughly comparable to Claude Fable 5.1..
Anthropic said Lean checked the finished proof using its three standard axioms, and a comparator confirmed that the theorem’s statement matched Mathlib’s statement of Fermat’s Last Theorem. The company said the proof is more than five times the size of Mathlib, the main community library of mathematical proofs on which the theorem builds..
Buzzard said automatic formalization of Fermat’s Last Theorem would be “a big step towards automatic formalization of the modern mathematical literature.” He said such techniques could help find errors in existing mathematical work and reduce the burden on referees.. Anthropic also said researchers using three personal Claude Max plans formalized Vinogradov’s Three Primes Theorem in three days through Prove2Me.
The company said it has expanded support for external researchers with free and discounted subscriptions, research credits and grants for larger scientific projects.. Featured image credit. Tags: claudeFermat’s Last Theorem
