Anthropic: Claude performs a computer-verified demonstration of Fermat's last theorem

According to the company, this is “a major step forward towards a future where all mathematics can be easily verified”. The American startup Anthropic, at the forefront of artificial intelligence (AI), announced that its Claude program had produced the "first complete and computer-verified demonstration of Fermat's last theorem", in a press release published Friday September 4.

Fermat's Last Theorem, conjectured by French mathematician Pierre de Fermat in 1637, is "one of the most famous mathematical conjectures of all time," explains Anthropic, which summarizes it this way: "No positive integer a, b, c satisfies the equation aⁿ + bⁿ = cⁿ for all n > 2." It took more than three centuries to obtain the first proof of this theorem, carried out by Sir Andrew Wiles in 1995; it “had 129 pages and required months of careful work to be verified,” says the startup.

“Understanding a novel result deeply enough to be sure of its accuracy can take months or even years of work.”

To speed up this long verification process, some have tried to "formalize" the demonstration, by producing it in a form readable by a computer (in particular thanks to the Lean assistant). It was at this stage that Claude impressed, according to Anthropic: "In 11 days, working largely autonomously, Claude produced the first computer-verified, end-to-end proof of Fermat's Last Theorem. In the process, he wrote 13 million lines of Lean code and demonstrated 29,500 intermediate theorems."

An “extraordinary feat”

“Dozens of Claude agents collaborated to define concepts, demonstrate intermediate theorems and use them to prove increasingly complex statements,” says the company. Several early attempts "failed" as officers "quickly lost track of the project's progress and stopped collaborating effectively." But through a collaboration with the Prove2Me platform, AI agents "completed the demonstration in just under two weeks, consuming approximately six billion output tokens from a general-purpose AI model dedicated to in-house research, roughly comparable to Claude Fable 5.1."

Kevin Buzzard, a mathematician at Imperial College London who has been leading a collective effort since 2024 to formalize this demonstration, hailed an “extraordinary feat”. “Such self-formalization techniques will lead to new tools, making it possible to eradicate errors in the current mathematical corpus and to lighten the workload of evaluators,” explains the specialist. Automation will also avoid being swamped with checking AI-generated results, "which is currently an extremely expensive human-led process," adds Kevin Buzzard.