Claude produces first fully computer-checked proof of Fermat's Last Theorem

Anthropic says its Claude AI system has produced the first complete, computer-checked proof of Fermat’s Last Theorem, a 17th-century conjecture that stumped mathematicians for more than 350 years. According to the company, Claude worked largely autonomously over 11 days to translate the proof into Lean, a programming language that checks each logical step of a mathematical argument the way a calculator checks arithmetic.

Pierre de Fermat wrote the theorem’s statement around 1637 in the margin of a book, claiming no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2. He said he had a proof that would not fit in the margin, but mathematicians now believe that original proof was flawed, since no elementary one has surfaced since. Andrew Wiles published the first accepted proof in 1995, a 129-page argument that took months to verify and required him to fix a gap discovered during peer review. Converting Wiles’s proof into a form a computer can verify, a process called formalization, was expected to take years; a community effort led by Kevin Buzzard at Imperial College London had been working on it since 2024 using Lean.

According to Anthropic, Claude’s version of the proof runs to 13 million lines of Lean code and includes 29,500 intermediate theorems, built on top of Mathlib, the community’s shared library of formalized mathematics. Dozens of Claude agents worked in parallel through a platform called Prove2Me, built by Anthropic researcher Tianyi Peng and collaborators at Columbia University, which tracked which theorems still needed proving and let agents pick up where others left off. Anthropic says earlier attempts without that coordination tool failed because agents lost track of the project’s state, though those failed efforts still contributed about 7% of the final proof’s code.

A mathematician’s reaction

Buzzard, who reviewed the finished proof, said in a statement shared by Anthropic that it proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics, and that the tools used to build it have reached the point where other researchers can build on them. Anthropic says the proof uses only Lean’s three standard axioms and that an automated comparator confirmed its statement of the theorem matches Mathlib’s own.

Anthropic frames the work as a step toward checking mathematical results by computer rather than by human referees alone, a process that traditionally takes years for complex proofs. The company says formalization does not replace proofs written for humans to read but could reduce the burden on referees and help verify claims made by AI systems as they produce more mathematics. Anthropic did not claim the work produced new mathematical knowledge; the theorem itself was already proven by Wiles three decades ago.

Anthropic says it separately used three personal Claude subscriptions to formalize Vinogradov’s Three Primes Theorem in three days via Prove2Me, suggesting smaller formalization projects may now be within reach of individual researchers. Anthropic and other AI labs have also expanded free and discounted subscriptions and research grants for mathematicians working on formalization, a sign of where the company expects this approach to be tested next.