Anthropic says its Claude AI has produced the first fully computer-checked proof of Fermat's Last Theorem, completing the work in 11 days largely on its own and writing what is now the longest math proof ever built.

A human-led project at Imperial College London has been working on this exact same task since 2024 and is not close to finished. Claude beat it to the finish line. Kevin Buzzard, the mathematician leading the Imperial project, reviewed Claude's proof and confirmed it holds up using nothing but math's most basic logical rules.

According to Anthropic, Claude wrote the longest math proof ever made and used it to formally prove Fermat's Last Theorem, a problem that stumped mathematicians for 358 years. The AI did it in 11 days, mostly on its own, producing 13 million lines of code that a computer can check line by line, instead of requiring trust in a mathematician's word.

Fermat's Last Theorem states that no three positive whole numbers can each be raised to a power higher than 2 and have the first two add up to the third. Pierre de Fermat scribbled that claim into the margin of a math book in 1637, adding that he had a "truly marvelous proof" that the margin was too small to fit. Then he died. Mathematicians spent the next 358 years trying to reconstruct whatever he thought he had.

Proving Something and Checking It Are Two Different Jobs

A math proof is a chain of logical steps, and if one link is broken, the whole thing collapses. Finding that single broken link, buried somewhere in a hundred pages of dense argument, can take other mathematicians years of their lives.

Formalizing a proof means translating it into a language so literal that a computer can verify every step on its own, without entering into subjectivities.

Mathematicians have struggled with verification for a long time. A 1908 German prize—worth roughly $1 million to $2 million in today's money, offered for the first valid proof of the theorem—drew 621 wrong submissions in its first year alone.

As Anthropic wrote on X:

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

The real proof did not appear until 1995, from British mathematician Andrew Wiles, and it came with a twist. Wiles announced his solution across three lectures in June 1993, only for a reviewer to later find a hole in it. He spent almost a year fixing it with a former student, Richard Taylor, nearly gave up, and finally published a corrected, 129-page proof in May 1995. It relied on mathematics that did not exist in Fermat's lifetime, which is a major reason mathematicians now doubt Fermat's own "marvelous proof" ever actually worked.

Computer-verified mathematics itself is decades old. The first famous case was the 1976 computer-assisted proof of the Four Color Theorem, which sparked ongoing debate over whether a proof no human can fully read by hand should count. Formal proof languages like Lean—created by Leonardo de Moura, originally at Microsoft Research—grew out of exactly that tension, letting software do the checking so humans can trust the result anyway.

In 2024, Imperial College London mathematician Kevin Buzzard kicked off a project to do exactly what Claude just did: translate Wiles's proof into Lean, a language computers can check. It is the kind of job that needs an army of volunteer mathematicians—the project's own outline runs 86 pages, and its funding is locked in through 2029. Claude finished the whole thing in 11 days.

How Claude Actually Pulled It Off

Anthropic explains in a more in-depth post that Tianyi Peng, who builds AI formalization tools with a team at Columbia, decided to see how far Claude could get on its own. Dozens of Claude agents worked in parallel, writing definitions, proving small results, and stacking those into bigger ones, with almost no human input beyond the occasional nudge like "prioritize this theorem next."

It did not go smoothly at first. Early on, the agents kept losing track of what they had already proven and stopped collaborating; those false starts still make up about 7% of the lines in the final proof.

What fixed it was a tool called Prove2Me, also built by Peng's team, which gave every agent the same live to-do list of which smaller proofs still needed doing, so nobody duplicated work or wandered off. It also organized files so Lean could check everything faster, and kept plain-English notes on each result so agents could reuse each other's work instead of reinventing it.

By the time it was done, Claude had proven more than 30,000 supporting theorems and burned through billions of tokens, running on a research model Anthropic says is roughly comparable to Claude Fable 5.1, the version it later released to the public. The finished proof runs 13 million lines—more than five times the size of Mathlib, the shared library mathematicians already use for this kind of work.

A typical novel runs 80,000 words. Claude's proof is equivalent to 160 novels of pure logical argument.

So Does This Actually Matter?

Buzzard—whose own version of this project remains funded through 2029—reviewed Claude's proof and gave it his blessing, saying it proves the theorem "with no assumptions other than the axioms of mathematics."

This is not the same as Claude discovering brand-new math, which Anthropic also claimed with its cryptography research earlier this year. Wiles already proved Fermat's theorem three decades ago—Claude built a machine-checkable receipt for it. That matters because mathematicians are increasingly swamped with unverified proofs, including AI-written ones, arriving faster than humans can check them by hand. Such formalized proofs are also deterministic and not prone to human error, which is very important in math.

This is not a new problem. A computer-assisted proof of the Kepler conjecture took four years before a review panel would only commit to being "99% certain," and Grigori Perelman's proof of the Poincaré conjecture took about as long to fully sink in.

Anyone unwilling to take Anthropic's word for it does not have to. The full 13-million-line proof is available on GitHub, free for any mathematician with enough free time to pick apart, line by line.