13 million lines; 29,500 theorems: AI tackles Fermat's Last Theorem in 11 days

Anthropic says Claude has formalised Fermat's Last Theorem in just 11 days, producing 13 million lines of Lean code and 29,500 intermediate theorems, turning a famous human proof into a computer-checked mathematical proof.

In Short

• Claude formalised Fermat's Last Theorem in 11 days using 13 million lines of Lean code
• The AI proof contains 29,500 intermediate theorems and is over five times Mathlib's size
• A mathematical project expected to take five years was completed by AI in just 11 days

Fermat's Last Theorem took mathematicians more than 350 years to crack. Andrew Wiles finally proved it in the 1990s after years of work.

Now, an AI has taken that human proof and turned it into something a computer can check, and it did so in just 11 days.

Anthropic says its Claude AI system worked largely autonomously with multiple AI agents to formalise the proof in Lean, a programming language designed to verify mathematical reasoning.

The result is staggering in size: 13 million lines of Lean code and 29,500 intermediate theorems used in the final proof. Anthropic says it is more than five times the size of Mathlib, the major community library of formalised mathematics.

AI DID NOT DISCOVER A NEW PROOF

There is an important catch. Claude did not solve Fermat's Last Theorem from scratch. Wiles and other mathematicians had already established the proof decades ago.

What AI has done is convert that enormously complicated human proof into a format that a computer can check step by step.

Think of it as taking a 100-plus-page mathematical argument written for humans and translating it into computer code where every logical move has to pass inspection.

THE 5-YEAR PROJECT THAT TOOK 11 DAYS

This is where the development gets particularly interesting.

Mathematician Kevin Buzzard at Imperial College London had been leading a multi-year effort to formalise Wiles' proof in Lean. The project was expected to take years. Anthropic says Claude completed the end-to-end formalisation in 11 days.

Dozens of AI agents worked on different pieces of the enormous task. They initially struggled to coordinate, but using the collaborative mathematical platform Prove2Me helped them keep track of which theorems needed to be proved next.

The finished work is now described by Anthropic as the largest Lean proof ever constructed.

WHY FERMAT'S LAST THEOREM MATTERS AGAIN

The bigger story isn't really Fermat's theorem.

It is whether AI can take complicated mathematics written by humans and turn it into machine-checkable mathematics at scale.

If that becomes routine, computers could help mathematicians verify lengthy proofs, catch errors and build new work on formally checked foundations.

So, after more than 350 years, Fermat's Last Theorem has given mathematics another surprise: the theorem was solved by humans decades ago, but AI may have changed how we check mathematics in the future.

- Ends