The last of Wiedijk’s 100 theorems falls to Anthropic

An internal Anthropic model working through the prove2.me platform has formalized a complete proof of Fermat’s Last Theorem in Lean. Anthropic announced the result on September 4. FLT was the last theorem still open on Freek Wiedijk’s list of 100 formalization challenges, so the announcement also retires a benchmark that has stood for 20 years.

The fullest outside account so far comes from Kevin Buzzard, who leads the Imperial College FLT project, an open-source effort to formalize the same theorem with EPSRC funding that runs to September 2029. In a post on his Xena Project blog on WordPress, he congratulates Anthropic and explains what the repository contains, how he checked it, and what it leaves for his own project. Technically, he adds, a coffee shop in Islington revealed the news on Instagram an hour before Anthropic’s official announcement.

Which proof the model formalized

The repository does not follow the modern proof Buzzard has been formalizing himself, which follows ideas of Khare, Taylor and others. Anthropic’s model followed the 1995 Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument, going through the Langlands–Tunnell theorem and Ribet’s level-lowering theorem.

To do that, the code develops two bodies of theory. The first is Fontaine theory, which the proof needs to study flat deformations of Galois representations. Roughly, these are the controlled ways a symmetry of number fields can vary while keeping the arithmetic properties the argument depends on. The second is enough of Mazur’s work on the Eisenstein ideal to show that no Frey curve can have a point of a given small prime order. A Frey curve is the elliptic curve built from a hypothetical counterexample to FLT, and the strategy is to prove that it cannot exist.

That Mazur step comes with a restriction. Buzzard writes that Anthropic’s proof only works for prime exponents above a certain bound. The smaller cases were already handled: Best, Birkbeck, Brasca and Rodriguez had formalized FLT for odd regular primes, and the smallest irregular prime is 37. “So it’s all good,” Buzzard writes.

How do you check 13.4 million lines?

Lean requires every step of a proof to be spelled out in a formal language, and a small trusted kernel then checks each step mechanically. What a human paper covers in a paragraph can take pages of Lean, TechTimes notes, and here that adds up to a repository Buzzard puts at over 13.4 million lines. TechTimes gives a rounder figure of 13 million.

Buzzard compiled the code base himself and ran comparator on it. Comparator is a tool that checks a formal development proves exactly the statement it claims to prove, with no extra assumptions slipped in. “It checks out,” he writes. The build is heavy: it takes nearly 20 times as long to compile as Lean’s mathematics library, on a machine with 96 cores. Anthropic also gave him access to a machine with 500G of RAM, and even there Lean is sluggish when he jumps between files in a repository this size. For browsing, Anthropic supplied HTML documents that he finds easier to explore in practice. You clone the repository and open them in a web browser.

Buzzard called the work “an extraordinary autoformalization achievement”, TechTimes reported.

Eleven days, after a false start

The run itself took 11 days. According to TechTimes, it began with Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, who set out in early August to see whether Claude could make progress on Buzzard’s project. The first attempt used a standard Claude Code multi-agent harness and failed. The agents made early progress, then lost track of the overall state of the project and stopped working together effectively. The run that succeeded went through prove2.me instead.

Buzzard describes the result as thousands of pages of literature formalized end-to-end “by some kind of AI swarm in an 11 day period”. He was given £1M to run his project over five years. “Anthropic took only 11 days but I do wonder if they spent more money,” he writes.

What is left for the EPSRC project

The obvious reading, that Buzzard now has nothing left to do, is one he rejects. The repository does more than he promised the EPSRC on one point: he only committed to reducing FLT to the 1980s, and Anthropic’s code proves the whole thing. But the grant covers two other things that the formalization does not touch.

• Pull requests to Lean’s mathematics library that add fundamental objects from modern number theory. That work is ongoing.
• A dynamic document that lets humans explore the modern proof. He calls this perhaps the most important deliverable, and guesses Anthropic is unlikely to build it: “they will feel that their job is done with the formalization”, and in any case they did not formalize the modern proof.

He is just as direct about the mathematics. “Mathematically this work of anthropic tells us essentially nothing,” he writes. He has said publicly that he is 99.9% sure the proof of FLT is correct, and most number theorists are 100% sure. As far as he understands the argument, the formalization “just faithfully follows the early literature on the proof and adds nothing.” In August, by contrast, a research version of Claude raised a lower bound on Riemann zeta zeros from 41.6% to 67.2%; the FLT run only re-derives, in Lean, a proof already in print.

Why he is excited anyway

For Buzzard, the news is about autoformalization: AI turning published mathematics into checked formal proofs. If an AI system can now do this to thousands of pages in 11 days, he expects to see modern research formalized “on the fly”. He also expects to learn whether his paranoia about the current state of the Langlands program is justified, as machines check it and “ruthlessly flag arguments which are incomplete.” Wiles’s 1995 proof ran to 129 pages, and a gap found during review took Wiles and Richard Taylor a year to fix, TechTimes recalls.

He sees two practical effects. Reviewing mathematics papers should become far less painful. And formalization should keep the field honest, because some papers assume results “known to the experts”, and he wants to see exactly what the proofs of important results in his field are assuming.

He ends the post with a story. In 1993 Wiles announced his proof in three lectures at the Newton Institute. Buzzard, then a second-year graduate student, attended the first, found it completely incomprehensible, skipped the other two and went on holiday to Ireland with his new girlfriend. He only learned the theorem had been proved when he got back to Cambridge a week later. This time Anthropic’s email reached him at the Green Man music festival in Wales, with the same girlfriend and very poor phone reception. During a brief moment of 4G he saw a message from someone he had never heard of, titled “End-to-end Lean formalization of Fermat’s Last Theorem”, and wrote the sender off as a crank. He found out what it was a week later, going through nearly 1,000 unread emails.