Claude Formalizes Fermat's Last Theorem

Anthropic says Claude has completed the first computer formalization of Fermat's Last Theorem: a version written in Lean that a computer can check step by step. The process took 11 days and produced around 13 million lines of mathematical code.

The result is not a new discovery about the theorem. Mathematician Andrew Wiles proved it in 1995, in a 129-page proof that required years of work and review. What Claude has done is turn that proof into instructions precise enough for a computer system to check its logic.

From a Note in a Book to Millions of Lines

Fermat's Last Theorem states that there are no positive integers satisfying aⁿ + bⁿ = cⁿ when n > 2. Fermat wrote the claim around 1637 and left behind a famous sentence: he said he had a proof that was too long to fit in the margin of the book.

For more than 350 years, no one found that proof. Wiles presented a proof in 1993, but mathematicians later identified a significant flaw. He took another year to fix it together with Richard Taylor. The definitive version was published in 1995 and used mathematical tools that did not even exist in Fermat's time.

Formalizing a proof means translating it into a language that does not allow steps to be skipped. Anthropic used Lean, a proof assistant that automatically checks whether each claim follows from the previous ones. A mathematical text can say “it is obvious” and move on. Lean requires that part to be proved too.

What Claude Did

The project started from a simplified version of Wiles's proof developed by Henri Darmon, Fred Diamond and Richard Taylor. Dozens of Claude agents worked together to define concepts, solve intermediate problems and connect the results until they reached the final theorem.

The system produced verifiable proofs for 30,300 theorems during the process. Of those, 29,500 are used in the final proof. The result is more than five times the size of Mathlib, the main community library of mathematical proofs in Lean on which the project relies.

The first attempts failed because the agents lost track of the state of the work and stopped coordinating. Progress came from using Prove2Me, a collaborative platform for formalizing mathematics created by Tianyi Peng and his colleagues at Columbia University.

In total, the team used around 6 billion tokens, the units models use to process and generate text. Anthropic says the proof uses only Lean's three standard axioms and that its formulation matches the version of the theorem included in Mathlib.

“If automated formalization of FLT is possible now, we have taken a major step toward the automated formalization of modern mathematical literature,” said Kevin Buzzard of Imperial College London after reviewing the work.

What This Changes for You

The significance is not that an AI has “surpassed” Wiles. It is that AI can help review complex proofs with a level of precision that would be very costly to achieve using human mathematicians alone.

A traditional proof can take months or years to evaluate. If it contains an error in a single step, everything that follows may be invalidated. A formalized proof allows Lean to check the complete logical chain, even though humans still need an understandable explanation of the ideas.

This could affect three areas:

• Scientific review: checking new results with less manual work.
• AI-generated mathematics: distinguishing between a convincing proof and one that actually works.
• Knowledge libraries: building reusable proofs so future work does not have to start from scratch.

There is an important difference: Claude has not found a new proof of Fermat's Last Theorem. It has automated a highly labor-intensive part of verifying a known proof. The next step will be to see how far this technique can go with other important results and whether formalizations can become smaller, clearer and easier to maintain.

Mathematics is not reduced to code, but code can become a second layer of trust. As AI systems produce more results, that layer could be the practical way to determine which ones deserve to be taken seriously.