What Happened
On September 4, 2026, Anthropic published the first complete, end-to-end machine-checked formalization of Fermat's Last Theorem. The work was carried out in Lean, a proof assistant that verifies mathematical arguments line by line against a small trusted kernel. Claude, running as a team of dozens of parallel agents, wrote roughly 13 million lines of Lean code over eleven days of wall-clock time, proving 30,300 theorems along the way, of which 29,500 appear in the final argument. The run consumed approximately six billion output tokens.
The distinction that matters here is between proving and formalizing. Andrew Wiles proved Fermat's Last Theorem in 1995, and the mathematical argument remains entirely his. What the eleven-day run produced was a translation of that 129-page proof — following the exposition by Darmon, Diamond and Taylor — into a language a computer can check mechanically, without depending on a human referee's judgment about whether a step really follows. No new mathematics was discovered. Something else was demonstrated: that the translation itself, long assumed to be a multi-year human undertaking, can now be done at machine speed.
The theorem's origin story is one of the most repeated in mathematics. Around 1637, Pierre de Fermat wrote in the margin of his copy of Diophantus's Arithmetica that no positive integers satisfy an + bn = cn for any integer n greater than two, then added that the margin was too narrow to contain his proof. Most historians now believe that proof, if Fermat ever had one in rigorous form, was wrong. The techniques required would not exist for another three and a half centuries.
The first attempt at the formalization failed. A standard multi-agent setup made early progress and then fell apart: with millions of lines of code and thousands of intermediate results in play, no single agent's context could hold the state of the project, and the agents began duplicating each other's work and overwriting each other's progress. The fix came from Prove2Me, an open-source formalization platform built by Tianyi Peng's group at Columbia University, which maintains a directed acyclic graph of every theorem statement in the project. Each theorem is a node; each dependency is an edge. Any agent joining the effort queries the graph to learn what has been proved, what is in progress, and what remains open.
Why It Matters
Mathematical verification has a scaling problem that predates artificial intelligence by decades. Wiles's original manuscript contained a gap that survived initial review; he and his former student Richard Taylor spent a year closing it. Thomas Hales's 1998 proof of the Kepler conjecture sat in review for four years before a twelve-referee panel could agree only that it was ninety-nine percent certain — Hales eventually organized a twenty-person formalization project to settle the matter. Grigori Perelman's proof of the Poincaré conjecture required the community roughly four years and three lengthy expositions before it was accepted.
Proof assistants were built to remove that bottleneck, and they do — but at a price. A step a human proof presents in a single paragraph may take pages of Lean to make explicit, because Lean cannot read between the lines or extend the benefit of the doubt. That labor cost is precisely why formalizing a proof as long and technically varied as Wiles's was expected to take years. Kevin Buzzard launched an EPSRC-funded five-year project at Imperial College London in 2024 to do exactly that, recruiting mathematicians worldwide and publishing an 86-page blueprint for the work. The plan ran through 2029.
It is worth being precise about what Lean's verification does and does not guarantee. It confirms that a proof follows from its stated definitions, axioms and prior verified results. It does not confirm that the definitions are meaningful, that the axioms are sound, or that the theorem statement was encoded to mean what its author intended. And trust in any Lean proof is conditional on trust in Lean's kernel, which is itself software. In the summer of 2026 a kernel soundness bug briefly allowed a spurious disproof of the Collatz conjecture to pass verification before it was found and fixed. Machine checking is a large improvement on human review. It is not an unconditional guarantee.
Reaction
Buzzard, whose community project was working toward the same milestone, reviewed the result and confirmed that it establishes the theorem with no assumptions beyond the standard axioms of mathematics. He also drew a wider conclusion: that if automatic formalization of a proof at this scale is possible now, the automatic formalization of the modern mathematical literature has moved considerably closer, bringing with it tools that could root out errors already sitting in the published corpus and lighten the burden carried by referees.
His praise came with a qualification that has been quoted less often. On the mathematics itself, Buzzard told Nature, the result changes nothing. The proof follows the 1995 exposition of the Wiles argument rather than the more modern route his own project has been formalizing. It is an engineering achievement in verification, not a contribution to number theory, and the distinction is not a small one for the mathematicians whose grant was written around the harder path.
The credit question is the part the mathematics community is still working through. Anthropic's own repository credits 106 upstream files to Buzzard's Imperial College project and to Mathlib contributors. Mathlib — the community-maintained library of formalized mathematics that the new proof builds on, and which that proof exceeds fivefold in sheer size — was assembled by hundreds of mathematicians over years of volunteer work. Prove2Me came from Columbia, not Anthropic. The Lean proof assistant is maintained by a nonprofit. Meanwhile, the Lean community's own framing of the milestone attributes it to Buzzard's project and records it as the final entry on Freek Wiedijk's hundred-problem challenge list, without mentioning Claude at all.
What's Next
Anthropic followed the main run with a deliberately modest experiment: three researchers, using ordinary consumer Claude Max subscriptions and collaborating through Prove2Me, formalized Vinogradov's Three Primes Theorem — a substantial result in additive number theory — in three days. The point was not the theorem. The point was that the scaffolding, not the compute budget, is what made the eleven-day run possible, and the scaffolding is open source.
The full proof is available on GitHub under an Apache 2.0 license alongside a written walk-through, and several labs have expanded support for external researchers working in pure mathematics and formalization through free or discounted access, research credits and dedicated grants. Whether that support reaches the community projects that made this possible, or routes around them, is an open question that funding bodies will answer over the next few cycles.
The deeper shift is to where the human bottleneck sits. If a system can produce both a proof and its formalization, the referee's job stops being the verification of every logical step and becomes something narrower and harder to automate: deciding whether the theorem statement, as encoded, actually means what it claims to mean. Anthropic expects formalized proofs to become a routine companion to write-ups intended for human readers. That would be a genuine change in how mathematics is published, and it would arrive without anyone having discovered anything new.
Closing Thoughts
There is a quiet irony in the shape of this result. The most famous unwritten proof in mathematics — the one Fermat claimed he could not fit in a margin — has now been answered by a proof so long that no margin, no book, and no human reading schedule could contain it either. Thirteen million lines is not a document anyone will read. It is an artifact designed to be checked rather than understood, and the only reader it was ever meant for is a program.
That is not a loss, but it is a change worth naming. Mathematics has always carried two things at once: the certainty that an argument holds, and the human comprehension of why it holds. Formalization separates them cleanly for the first time, and it turns out you can have a great deal of the first with almost none of the second. The eleven-day proof is certain in a way Wiles's manuscript was not on the day it was submitted. It is also, as a piece of writing, nearly meaningless to a person.
What the mathematical community does with that separation is the interesting part, and it is not primarily a technical question. It is a question about whose labor gets recognized when infrastructure built over years by volunteers becomes the substrate for a result announced in eleven days — and about whether the tools that follow will be built to serve the people who write proofs, or to route around them. Fermat's margin note survived for three and a half centuries because it was short enough to keep repeating. Nothing about the current moment is short enough to repeat, which may be exactly why it deserves the attention.
한글 요약
앤트로픽이 2026년 9월 4일 페르마의 마지막 정리에 대한 최초의 완전한 기계 검증 형식화 결과를 공개했습니다. Lean 증명 보조기 언어로 약 1,300만 줄의 코드가 11일 만에 작성됐고, 그 과정에서 3만 300개의 정리가 검증됐습니다. 다만 이는 새로운 수학이 아닙니다. 1995년 앤드루 와일스가 이미 증명한 129쪽짜리 논증을, 컴퓨터가 한 줄씩 기계적으로 확인할 수 있는 형태로 옮긴 형식화 작업입니다. 첫 시도는 실패했고, 컬럼비아대 연구진이 만든 오픈소스 플랫폼 Prove2Me가 정리 간 의존 관계를 그래프로 관리하면서 비로소 완주가 가능해졌습니다.
이 성과를 검토한 임페리얼 칼리지 런던의 케빈 버자드 교수는 결과 자체가 수학의 표준 공리 외에 어떤 가정도 없이 정리를 확립한다고 확인했습니다. 동시에 그는 이것이 수학 자체에 관해서는 아무것도 바꾸지 않는다는 점도 분명히 했습니다. 2024년부터 5년 계획으로 같은 목표를 향해 온 그의 커뮤니티 프로젝트는 더 현대적인 경로를 형식화해 왔는데, 이번 결과는 1995년 방식의 해설을 따랐기 때문입니다. 앤트로픽 저장소는 106개 상위 파일을 버자드 프로젝트와 Mathlib 기여자들에게 귀속시켰지만, 수년간 자원봉사로 쌓인 공동 인프라 위에서 나온 성과의 공로를 어떻게 배분할 것인가는 아직 정리되지 않은 문제로 남아 있습니다.
후속 실험에서는 일반 소비자용 구독 세 개만으로 비노그라도프의 세 소수 정리를 사흘 만에 형식화했습니다. 결정적인 요소가 막대한 연산 자원이 아니라 오픈소스로 공개된 협업 구조였다는 뜻입니다. 앞으로 바뀌는 것은 검증의 병목 지점입니다. 논증의 모든 단계를 사람이 따라가는 대신, 정리의 서술이 정말 의도한 의미를 담고 있는지를 판단하는 쪽으로 심사의 무게중심이 옮겨갑니다. 페르마가 여백이 좁아 적지 못했다던 증명은, 이제 어떤 여백에도 담기지 않는 1,300만 줄로 답을 얻었습니다.