Claude Confirms Fermat's Last Theorem Correct; Sir Andrew Wiles Had Also Done This, in 1995

SAN FRANCISCO — Anthropic announced Monday that its Claude AI had autonomously formalized Fermat's Last Theorem in the Lean 4 proof-checking language over 11 days, confirming to the satisfaction of a computer that the theorem is correct — a question the mathematics community considered definitively answered in 1995, when British mathematician Sir Andrew Wiles published the 129-page proof that answered it.

The model, operating without sustained human instruction via the Prove2Me platform, generated 13 million lines of Lean code and discharged 30,300 subsidiary theorems before the Lean kernel confirmed the result. Claude consumed approximately six billion output tokens in the process. Wiles consumed approximately 129 pages.

"This is a landmark in formal mathematics," Anthropic said in a blog post, crediting the achievement to Claude. Wiles, who received the Abel Prize, the Wolf Prize, and the Royal Medal for the same problem, was not mentioned.

A number theorist at MIT, reached by someone who still had her department's phone number, called the Lean formalization "genuinely difficult and important work" and "not quite the same as proving Fermat's Last Theorem." She said explaining the distinction to people who read AI press releases had become, over the years, its own open problem.

With Fermat complete, Claude has been assigned the remaining items in its formal-verification queue: the Pythagorean theorem, the irrationality of the square root of two, and a formalization of Euclid's proof that infinitely many primes exist — a result Euclid established around 300 BCE using no proof checker and considerably fewer tokens.

"We have a backlog," said a person familiar with the matter.

Wiles has not been notified that his proof has been verified. He is believed to be fine.