A research post published by Anthropic on September 4, 2026 under its Science section, reporting what it calls "the first complete computer-checked proof of Fermat's Last Theorem." The proof was written in the Lean proof assistant by Claude agents working "largely autonomously over 11 days," and is published as a repository at github.com together with a written walk-through.
What the post claims and does not claim
The post's central qualification is stated in its own terms and is the load-bearing part of the result: "Unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what's novel here is the verification." The theorem proved is Andrew Wiles's, published in May 1995 and running to 129 pages; the contribution is the machine-checkable encoding of that proof rather than a new argument. The post is explicit that Claude's proof "follows a simplified version of Wiles's proof from Darmon, Diamond and Taylor," citing the expository paper by Henri Darmon, Fred Diamond and Richard Taylor.
Background as the post gives it
Fermat recorded the conjecture around 1637 in the margin of his copy of Diophantus's Arithmetica. The post notes that in 1908 a prize of 100,000 German gold marks — which it puts at the equivalent of one to two million dollars today — was announced for a correct proof, and that 621 incorrect attempts were produced in the first year alone. Wiles presented a proof in June 1993 over a three-day lecture series; two months into verification a reviewer exposed a gap, which Wiles spent a year repairing, first alone and then with his former student Richard Taylor, before publishing the corrected proof in May 1995. Because no elementary proof has been found, the post states, "the mathematical community now believes Fermat's own original 'marvelous proof' was incorrect."
Formalization of Wiles's proof was proposed a decade after publication by the Dutch computer scientist Jan Bergstra. A multi-year community effort to complete it in Lean was begun in 2024 by Kevin Buzzard at Imperial College London; the blueprint describing only the initial phase of that project runs to 86 pages, and the post says the full formalization "was expected to take years."
Scale and method
| Measure | Value as stated |
|---|---|
| Elapsed time | 11 days |
| Lines of Lean produced | 13 million |
| Theorems proved along the way | 30,300 |
| Theorems used in the final proof | 29,500 |
| Output tokens consumed | about six billion |
| Model | a general-purpose internal research model "roughly comparable to Claude Fable 5.1" |
| Size relative to Mathlib | over 5× |
The post attributes the size ratio partly to Mathlib being "concise and well-reviewed, while our proof is likely much longer than it needs to be." Dozens of Claude agents worked in parallel to define concepts, prove intermediate theorems, and build toward harder statements. Human mathematical input is described as "limited to occasional high-level instructions" from Tianyi Peng, quoted as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon."
The finished proof was checked by Lean, uses only Lean's three standard axioms, and a comparator tool confirmed that the theorem statement matches Mathlib's own statement of Fermat's Last Theorem.
The role of Prove2Me and the early failures
The post records that initial attempts failed: "while agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively," and those failed efforts contributed roughly 7 percent of the non-boilerplate lines in the final proof. The effort succeeded after the team moved to Prove2Me, described in the post as "an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University." Three mechanisms are credited: a directed acyclic graph of theorem statements that agents used to choose what to attempt next, which the post says mitigated memory degradation and allowed parallel work; separation of theorem statements from proofs into different files, speeding Lean compilation and lowering resource consumption; and a natural-language description attached to each statement, enabling search and reuse.
The post introduces Peng as "an Anthropic researcher whose group at Columbia University builds tools for AI formalization." The arXiv paper describing the platform lists his affiliation as Columbia University's Graduate School of Business and gives no Anthropic affiliation for any author.
Excerpts of the agents' reasoning are published as a separate PDF; the post quotes three, including "🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17)."
Reception
Kevin Buzzard reviewed the proof and is quoted twice. On the result itself: "This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered." On what follows: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees. The techniques will also enable us to rigorously check LLM-generated mathematics, which is currently typically an extremely costly human-led process."
Anthropic's stated implications
The post argues that formalization at this speed makes it possible "to formalize large swaths of mathematics," which may catch errors in the existing corpus and reduce the refereeing burden, and that as AI-produced proofs multiply, "it will become common to produce a formalized proof alongside any write-up intended for a human reader" — while stating that a formalized proof should not replace a human-understandable exposition. It also reports that writing Lean "seems to help Claude prove novel results," with recent Claude-authored results formalized in parallel with their proofs and the partial proofs used by the model to check its own hypotheses.
A second, smaller experiment is reported: Anthropic researchers used three personal Claude Max plans, collaborating entirely through Prove2Me, to formalize Vinogradov's Three Primes Theorem in three days, from which the post concludes that "collaborative formalization of major results with consumer AI subscriptions is achievable." The post notes Anthropic's expanded support for external researchers through free and discounted subscriptions, research credits and dedicated AI-for-science grants, and points to comparable programs at other labs.
Anthropic's stated position on the broader question is narrow: "Formalization, however, is a place where we feel unambiguously good about the role of AI," linking to the Leiden Declaration on Artificial Intelligence and Mathematics as evidence that mathematicians are contesting AI's role in their field more generally. The Declaration itself treats formalization as a site of the problem rather than an exception, stating that unreliable arguments are hard to distinguish from correct proofs "not only [for] informal arguments, but also to formalizations, where the difficulty lies in the translation between computer-encoded and human presentations of concepts" (Leiden Declaration on Artificial Intelligence and Mathematics (2026)).
Acknowledgments and lineage
The post credits Wiles and Taylor's proof as a culmination integrating work by Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Barry Mazur, Robert Langlands, Jerrold Tunnell, Yutaka Taniyama, Goro Shimura and André Weil, among others. Claude's proof adapts pieces from the Imperial College London FLT project led by Buzzard and from the flt-regular project. Anthropic thanks Buzzard for reviewing the proof.
Two footnotes supply the framing for why verification matters. One records that Peng, as an undergraduate, told his research advisor he was "99% sure, but it's hard to be 100% certain about a proof this long," and consequently missed inclusion in a Nature article. The other lists comparable verification struggles: Thomas Hales's 1998 Kepler conjecture proof, four years in review before a twelve-referee panel settled for "99% certain" and later formalized through the twenty-person Flyspeck project; Grigori Perelman's 2002 Poincaré conjecture proof, taking roughly four years and three 300-page expositions to be accepted; and Harald Helfgott's 2013 weak Goldbach proof, described as still under review.
Relationships
- depends-on: Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)
- supports: Autoformalization and Machine-Checked Proof
- supports: AI for Science
- related: Anthropic
- related: Claude Fable 5.1
- related: Ten Advances in Mathematics and Theoretical Computer Science
- related: Verification Asymmetry
- related: Agentic AI