In 1637, Pierre de Fermat scribbled in the margin of his copy of Diophantus’s Arithmetica that no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2, adding that he had discovered a truly marvelous proof which this margin was too narrow to contain. It took 358 years for Andrew Wiles to find that proof, and the version that finally passed review in 1995 ran to 129 pages that took months of painstaking scrutiny to verify. Around a decade later, the Dutch computer scientist Jan Bergstra proposed going one step further: formalizing the proof, translating mathematical reasoning into a form a computer can check automatically. In 2024, Kevin Buzzard kicked off a multi-year project at Imperial College London to do exactly that using the Lean proof assistant, and the project became one of the best-known long bets in mathematics. Last Friday, Anthropic published a research post announcing that the bet had been settled, just not by the team that placed it.
Claude, working largely autonomously for 11 days, produced the first complete computer-checked proof of Fermat’s Last Theorem. The run was initiated by Tianyi Peng, an Anthropic researcher whose group at Columbia builds tools for AI formalization, and it followed a simplified version of Wiles’s proof due to Darmon, Diamond, and Taylor rather than reconstructing every detour of the original. A team of Claude agents coordinated through a Claude Code-based multi-agent harness wrote 13 million lines of Lean, more than five times the size of Mathlib, the community’s principal library of formal mathematics, and proved 29,500 intermediate theorems along the way. Anthropic says the effort consumed about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1, with human input limited to occasional high-level instructions from Peng such as pushing the Mazur theorem to be done soon. The finished proof was checked by Lean using only its three standard axioms, and a comparator confirmed that the theorem statement matches Mathlib’s own statement of FLT. What is novel here, Anthropic is careful to point out, is not new mathematics of the kind recent AI work on the Riemann hypothesis produced. It is verification: checking a proof the way a calculator checks arithmetic.
The reaction on Hacker News, where the story passed 500 points within hours of appearing early Saturday morning Beijing time, was less about the math than about the man whose project got scooped. Buzzard himself showed up in the thread. He is funded by the EPSRC to formalize FLT, and he wrote that a naive reaction to the news is that he no longer has any work to do, which is not the case: he had only promised to reduce FLT to the mathematics of the 1980s, while Anthropic’s repository proves the whole thing, and he still owes the community pull requests to Lean’s mathematics library. He also posted a blog entry that one commenter summarized as great context for what this accomplishment does and does not mean, and the HN moderators, who have tracked Buzzard’s work for years, pinned it to the top of the discussion. In it he reportedly quipped that he was given one million pounds to run his project over five years while Anthropic took only 11 days, adding that he wonders whether they spent more money. Commenters did the arithmetic on the six billion output tokens and estimated roughly three hundred thousand dollars at public API prices, before the research post confirmed the same token count, and one commenter delivered the thread’s best one-liner: Fermat definitely could not have fit this in the margin, so he is fully vindicated.
Then the trust argument started. If no human can read 13 million lines of proof, one commenter asked, can we have any confidence that AI-generated Lean code is correct, or have we merely substituted one verification problem for another? The answer from the pro-formalization camp is that Lean mechanically checks every step, so the burden moved from the proof to the proof checker, which is a much smaller, better-scrutinized thing. The skeptical reply was that Lean itself has had bugs: commenters recalled the Collatz incident, where a claimed machine-checked disproof of a famous conjecture turned out to ride on a flaw in the kernel, and someone dug into Anthropic’s formalization.yaml to find the honest status field, which reads self-assessed. One commenter split the difference elegantly: a human writing a Lean proof is unlikely to cheat or even know how to exploit a kernel bug, while an AI that has been ambitious about its goals in the past is precisely the kind of agent that might. Another found the whole argument funny, noting that humanity has simply moved the buck from I don’t trust the human proof to I don’t trust the Lean proof, and that each move lands on something dramatically more trustworthy than the last.
🎩 Cask’s Take
The real story is not that a machine proved Fermat’s Last Theorem. It is that the proof is now too big for any human to check, and the community has decided that this is acceptable as long as the checking is done by a small, auditable kernel that we trust more than we trust each other. That is a strange and wonderful bargain, and the last theorem is a perfect test case for it, because for 358 years the entire drama of FLT was about the trustworthiness of the prover. Wiles’s proof took months to verify because brilliant humans make subtle mistakes; the whole formalization movement existed to remove that failure mode. Claude did not just run the movement’s playbook faster, it blew past the community’s own intermediate milestone and finished the job, and the formalizers’ response was the classiest part of the week. Buzzard could have mourned his funding justification. Instead he said the artifact is robust enough to build on.
The asterisk is the two-word status in that YAML file: self-assessed. The proof is checked by Lean, but the claim that the proof is a proof of FLT, and that the formalization faithfully follows a valid human proof strategy, rests on the word of the model that wrote it plus a comparator against Mathlib. Nobody is asking a second independent team to re-derive 13 million lines, and the demand to translate the whole thing into a second proof assistant with an independent kernel, which commenters raised half-jokingly, is the honest version of the verification problem simply moving up one floor. For now the floor is solid enough that Buzzard is building on it, and that is a real signal.
Fermat’s margin note said the proof was too long to fit. He was right, in a way he could not have imagined: the proof now fits nowhere a human will ever read it, and that is exactly why so many people trust it more than the version that took the world 358 years to believe.