An AI Formalized and Verified Fermat’s Last Theorem in 11 Days, a Task Expected to Take Years

Claude did not rediscover the proof. It made the existing one machine-checkable.

Andrew Wiles spent seven years trying to solve a mathematical problem that had resisted everyone else for more than three centuries. When he finally announced a proof of Fermat’s Last Theorem in 1993, mathematicians found a flaw that took another year to fix with the help of collaborator Richard Taylor.

Now, more than 30 years later, an artificial intelligence system from Anthropic has taken this famously difficult proof and turned it into something a computer can verify from start to finish — in just 11 days. For comparison, a group of human mathematicians previously embarked on a 5-year-long project to perform the same task.

Anthropic says dozens of Claude agents converted the argument into 13 million lines of Lean, a formal language that checks mathematical logic step by step. The system proved more than 30,000 intermediate theorems along the way, using 29,500 of them in the final construction.

Claude did not independently solve Fermat’s Last Theorem, just so we’re on the same page. Wiles and Taylor did that in the 1990s. Instead, Claude turned an accepted human proof into a computer-verifiable one — an extremely laborious task in and of itself.

The feat suggests AI could make it practical to check enormous mathematical arguments automatically, including new proofs that humans do not yet know whether to trust.

The result “just completely blew my mind,” Alex Kontorovich, a number theorist at Rutgers University, told Nature.

Fermat’s Last Theorem

Fermat’s Last Theorem says no positive whole numbers a, b and c satisfy aⁿ + bⁿ = cⁿ when n is greater than 2. Pierre de Fermat made the claim in 1637 and famously suggested that he had found a proof too large for the margin of his book.

Pierre de Fermat first posed the problem in the 17th century while reading Arithmetica, an ancient Greek mathematics book by Diophantus. In the margin beside a problem about writing a number as the sum of two squares, Fermat scribbled a much broader claim: that no similar equation involving cubes, fourth powers or any higher powers could have whole-number solutions. He then added a tantalizing remark. He said he had found a “truly marvelous proof,” but that the margin was too narrow to contain it.

×

Get smarter every day...

Stay ahead with ZME Science and subscribe.

Daily Newsletter
The science you need to know, every weekday.

Weekly Newsletter
A week in science, all in one place. Sends every Sunday.
No spam, ever. Unsubscribe anytime. Review our Privacy Policy.

Thank you! One more thing...

Please check your inbox and confirm your subscription.

That entire, formal proof was never found. Fermat died without publishing one, and later mathematicians increasingly doubted that he had actually possessed a valid proof for the general case. The brief and very frustrating marginal note nevertheless launched one of mathematics’ longest-running puzzles, surviving for more than 350 years before Andrew Wiles finally proved the theorem.

Wiles’ proof connected branches of mathematics that had once seemed far apart, work that later earned him the prestigious 2016 Abel Prize. But mathematical proofs are written to be read and verified by other humans. Mathematicians skip steps they consider obvious, cite results proved elsewhere and rely on layers of shared background knowledge. But sometimes a wrong assumption can bring the whole argument crashing down.

A computer cannot do that.

What does it mean to verify a proof with code?

To formalize a proof, every definition, assumption and logical step has to be translated into a strict language the machine understands. Even steps that seem obvious to an expert must be spelled out. The computer then checks the argument line by line and refuses to accept it if any step does not follow from what came before. In the mathematical community, the go-to software for this task is called Lean.

That is what Claude did with Fermat’s Last Theorem. It took the accepted human proof and rebuilt it in Lean until the computer could verify the entire chain without having to trust the mathematicians who wrote it.

Kevin Buzzard, a mathematician at Imperial College London, has led a human-run Fermat formalization project since 2024. His effort also aims to create reusable mathematical tools and a proof that people can explore and learn from. Claude overtook the end-to-end certification goal at startling speed.

Before Claude’s run, Buzzard told Nature he was “99.9% sure that the proof was correct.” Afterward, he said, “I am now 100% sure”.

AI is moving from solving problems to checking mathematics

The automation of proof formalization could greatly accelerate research in mathematics, which in turn might accelerate the development of other applications. That includes AI itself because its bedrock is math.

In February, an AI system called Gauss helped complete a Lean formalization of Maryna Viazovska’s Fields Medal-winning solution to the sphere-packing problem in eight dimensions.

Then in August, OpenAI said an internal model had produced new results on ten long-standing problems in mathematics and theoretical computer science before formalizing each argument as a Lean certificate. Those results involved mathematical discovery as well as verification, making them importantly different from Claude’s work on Fermat.

“If they can formalize Fermat’s last theorem, they can probably formalize anything,” Daniel Litt, a number theorist at the University of Toronto, told Nature.

Yet Anthropic’s experiment also revealed how difficult autonomous mathematical work remains. Early groups of Claude agents lost track of the project and stopped coordinating. Researchers made progress only after moving them onto Prove2Me, a platform that mapped thousands of dependent subproblems so agents could track completed work and choose what to tackle next.

The run consumed about six billion output tokens. That adds up to roughly $300,000 at Anthropic’s published commercial rate, although its internal cost is likely much cheaper. As AI compute becomes increasingly cheaper, more and more institutions and research groups will be able to afford to formalize their math.

The catch is that a correct proof is not necessarily a useful one

Claude’s formalization of Fermat’s proof is enormous — more than five times the size of Mathlib itself. And Claude did not produce those 13 million lines primarily as a clean, reusable foundation for future mathematics.

Mathematicians do not want every new formal proof to rebuild the same basic machinery from scratch. They rely on shared libraries such as Mathlib, where definitions and previously proved results are organized so that later projects can reuse them.

Buzzard told Nature that mathematicians might be able to salvage parts of the code for Mathlib, but cleaning, reorganizing and integrating it could require a great deal of human effort. The risk is that future AI systems could produce thousands of correct proofs that each come with their own sprawling, incompatible collection of supporting mathematics. In that scenario, computers could verify individual results, but mathematicians would struggle to build on them efficiently. Buzzard called that possibility a “nightmare scenario.”

RelatedPosts

AI-designed autonomous underwater glider looks like a paper airplane and swims like a seal
Google’s DeepMind builds AI that helps archaeologists piece together Roman writings
Scientists Use AI to Create First-ever Functional Synthetic Life, Because What Could Go Wrong?
We Don’t Know How AI Works. Anthropic Wants to Build an “MRI” to Find Out

It’s this concern that explains Buzzard’s seemingly contradictory reaction. On his Xena blog, he wrote that “mathematically this work of Anthropic tells us essentially nothing.” Mathematicians already accepted the underlying proof.

Yet in Anthropic’s announcement, Buzzard was also quoted as saying the achievement “a big step towards automatic formalization of the modern mathematical literature.”

More about possibilities than what was done

The bigger prize may therefore have little to do with proving famous old theorems again. Formalization could give mathematics something it has never had at scale: an automated second reader that never tires and can identify exactly where an argument fails.

That could become crucial as mathematical papers grow longer and AI systems begin producing more of them. Frederick Manners, a mathematician at the University of California, San Diego, told Nature that “peer review has become more time-consuming but performed worse.” Eventually, mathematicians could publish a machine-checkable certificate alongside a human-readable proof, much as software developers use automated tests to check code.

For Fermat’s Last Theorem and the rather small number of nerds who care deeply about it, the verdict sounds almost anticlimactic: Wiles and Taylor were right.

The more consequential result is that researchers have now demonstrated, in days, a job once expected to consume years of expert labor. “Two years ago, that was a fantasy,” Buzzard said.