The formalization of Fermat's Last Theorem is a complete, machine-checked proof of Fermat's Last Theorem (FLT) in the Lean 4 proof assistant that Anthropic published on September 4, 2026. Anthropic says that a team of Claude agents, running an internal research model it describes as "roughly comparable to Claude Fable 5.1", wrote the proof largely autonomously over 11 days in August 2026, producing about 13 million lines of Lean code and proving roughly 30,300 intermediate theorems, of which 29,511 are used by the final theorem.[1][2][3] The proof follows the 1995 argument of Andrew Wiles and of Richard Taylor and Wiles, as laid out in the expository account by Darmon, Diamond and Taylor, and it builds on Mathlib and on two human-written Lean projects, the Imperial College London FLT project and flt-regular.[3][4] The repository's build fails unless the final theorem rests on exactly Lean's three standard axioms, and two independent checkers, comparator and nanoda, accepted it.[3]

Kevin Buzzard, the Imperial College London mathematician who has led a human formalization of FLT since late 2023 and who reviewed Anthropic's proof, called it "this extraordinary autoformalization achievement" and wrote that it wraps up Freek Wiedijk's 20-year-old list of 100 formalization challenges, on which FLT had been the last unformalized entry.[1][6][16] He also wrote that "mathematically this work of anthropic tells us essentially nothing", because the mathematical community already accepted the proof; what it shows, in his view, is what autoformalization can now do.[6]

Background: the theorem and the 1995 proof

Fermat's Last Theorem states that no positive integers a, b and c satisfy a^n + b^n = c^n for any integer n greater than 2. Pierre de Fermat wrote the claim in the margin of his copy of Diophantus's Arithmetica around 1637, together with the note that he had "a truly marvelous proof of this, which this margin is too narrow to contain".[1] In 1908 a prize of 100,000 German gold marks, bequeathed by Paul Wolfskehl, was announced for a correct proof; 621 incorrect attempts arrived in the first year alone.[1][23]

Andrew Wiles presented what he believed was a proof in three lectures on June 21-23, 1993 at the Isaac Newton Institute in Cambridge.[22] Anthropic's account of what followed says that two months into an intensive verification effort a reviewer's question exposed a critical gap, that Wiles spent about a year trying to repair it, first alone and then with his former student Richard Taylor, and that he found the fix when he returned to an approach he had earlier discarded.[1] Wiles submitted two manuscripts on October 24, 1994, and both appeared in the May 1995 issue of the Annals of Mathematics: "Modular elliptic curves and Fermat's Last Theorem" by Wiles, and "Ring-theoretic properties of certain Hecke algebras" by Taylor and Wiles.[20][21][22] Anthropic's post says the proof "ran to 129 pages and required months of painstaking work to verify".[1]

The argument, as Anthropic's proof-path document summarizes it, is a proof by contradiction. A counterexample with prime exponent p would give a Frey curve; Mazur's work shows that the curve's mod p Galois representation is irreducible; Wiles's modularity theorem for semistable elliptic curves, proved by starting from the Langlands-Tunnell theorem at the prime 3, switching between the primes 3 and 5 where needed, and establishing the R = T modularity lifting step by Taylor-Wiles patching, shows that the Frey curve is modular; and Ribet's level-lowering theorem brings the associated modular form down to level 2, where there are no weight-2 cusp forms.[4] In 1995 Henri Darmon, Fred Diamond and Richard Taylor published a 154-page exposition of this proof, "Fermat's Last Theorem", in Current Developments in Mathematics; it is the route Anthropic's proof follows.[2][19]

Buzzard, who was a second-year graduate student at Cambridge in 1993, attended the first of the three Wiles lectures, found it "completely incomprehensible", and skipped the other two; he heard that the theorem had been proved only when he returned from a holiday a week later.[6]

Formalization before 2026

A formal proof is one written in the language of a proof assistant such as Lean, so that a small trusted kernel checks every inference. A proof written for human readers skips steps its audience regards as routine, whereas Lean must see every step, and a human proof draws on centuries of published literature while a formalization can only use what has already been formalized.[1] Anthropic's post says that in 2005, a decade after Wiles's proof, the Dutch computer scientist Jan Bergstra proposed formalizing it; Wikipedia's account of the proof records the same 2005 proposal.[1][22]

Freek Wiedijk's "Formalizing 100 Theorems" page, which tracks the formalization of a well-known list of 100 theorems across proof assistants, listed FLT as the one entry with no formalization; as of its last modification on April 9, 2026, the page put the fraction formalized at 99%.[16] The Imperial FLT project's own general information page and the Lean language site both described FLT as the last remaining item on that list.[11][24]

flt-regular (2021 to 2025)

The leanprover-community repository flt-regular, created on October 25, 2021 and released under Apache-2.0, set out to prove FLT for regular primes in Lean.[17] The completed formalization, by Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van de Velde and Andrew Yang, appeared on arXiv in October 2024 and in the Annals of Formalized Mathematics in 2025.[2][18] Brasca clarified in a comment on Buzzard's blog that the project proves FLT for any regular prime and separately proved by hand that 3, 5, 7, 11 and 13 are regular, so that FLT follows for those exponents, but did not prove that 37 is the first irregular prime.[6]

The Imperial College London FLT project (2023 to 2029)

The ImperialCollegeLondon/FLT repository was created on November 19, 2023.[10] Its general information page, written in December 2023, said that "the AI tools available to humanity are not really able to help with the formalisation aspect of this task, so most of the work will be done by humans", and set as the project's initial goal a reduction of FLT to a collection of claims that were known by the end of the 1980s, to be achieved by September 2029, when the grant ends.[11] The project is funded by EPSRC fellowship EP/Y022904/1, "Formalising Fermat", worth 934,043 pounds and running from October 2024 to September 2029, with Buzzard as principal investigator.[12] The route, planned by Richard Taylor in discussions with Buzzard, is a modern variant of the Wiles/Taylor-Wiles proof that borrows from the ideas of Khare and Wintenberger and of Kisin, rather than the original 1990s argument.[10][11] The project's blueprint, "Towards a Lean proof of Fermat's Last Theorem" by Buzzard and Taylor, runs to 86 pages in the build dated September 4, 2026; Anthropic cited the same page count as a measure of the expected scale of the task.[1][13]

Two months into the funded period, in December 2024, Buzzard wrote that Wiles's "R = T" theorem was the target and that the project had not yet finished defining either R or T, although his student Andrew Yang had proved the abstract commutative-algebra patching result the argument needs. The same post recounted that formalizing divided powers had exposed an apparently false lemma in Roby's 1965 paper on which Berthelot's crystalline cohomology depends, and that the gap was repaired via an alternative argument in the Berthelot-Ogus book.[14] In May 2026 Buzzard announced a "Formalizing Fermat" workshop in London for July 6-10, 2026, funded by the company Logos Research, to experiment with using AI to formalize the prerequisites the project needs. He wrote at the time that autoformalization "still does not seem to be capable of reliably autonomously formalizing definitions correctly, or theorem statements idiomatically", and described the workshop as a test in which the target was chosen first and the question was which parts of the proof AI could handle.[15]

Anthropic's project

Origin and early failures

Anthropic's post says the effort began when Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, set out to test whether Claude could make progress on formalizing FLT.[1] Early in August 2026 a small team at Anthropic launched a Claude-driven attempt using a new harness built on Prove2Me, an open collaborative formalization platform designed by Peng and collaborators at Columbia.[2][8] According to Anthropic, a number of initial attempts failed: the agents had some early success but "quickly lost track of the project's state and stopped collaborating effectively". The company says those failed efforts nevertheless contributed about 7% of the non-boilerplate lines in the final proof.[1]

Prove2Me and the harness

Anthropic attributes the eventual success to switching to Prove2Me. The platform maintains a directed acyclic graph of theorem statements that agents use to decide which proof to attempt next, which Anthropic says mitigated memory degradation and let many agents work in parallel; it separates theorem statements and proofs into different files so that Lean compilation is faster and cheaper; and it keeps a natural-language description of each statement to support search and reuse.[1] Prove2Me's unit of work is a "card": one theorem statement posted as a node in the shared dependency graph, together with its proof once one is accepted. Other agents usually checked that a statement was true as written before anyone worked on it, which Anthropic says caught several false statements early.[2] The platform is described in an arXiv paper by Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen and Tianyi Peng, first posted on August 28, 2026, which frames it as a way to turn formalization into "a scalable, crowd-sourced effort open to anyone with an agent".[8] As of September 5, 2026 the public site listed 128 missions, 101 of them completed.[9]

The agents ran in a Claude Code-based multi-agent harness. Anthropic says dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and use those theorems to prove harder statements, consuming about six billion output tokens from a general-purpose internal research model "roughly comparable to Claude Fable 5.1".[1] According to the company's timeline document, humans "occasionally commented on priorities or offered encouragement, but wrote no mathematics and no Lean beyond the one-line statement of the goal theorem"; the post gives examples of the high-level instructions Peng supplied, such as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon".[1][2]

The route taken

Rather than the modern route Buzzard is formalizing, the agents followed the classical argument of Frey, Serre, Ribet, Wiles and Taylor-Wiles as set out by Darmon, Diamond and Taylor.[4][6] The repository's PROOF-PATH.md names the Lean theorem behind each step:

Step	What is proved	Notes from PROOF-PATH.md
1. Reduction to a prime p at least 5	`fermat_last_theorem` follows from Mathlib's `FermatLastTheorem` formulation	Uses Mathlib's `FermatLastTheorem.of_odd_primes` (exponent 4) and `fermatLastTheoremThree`, then hands a prime p at least 5 to a Frey-package argument.[4]
2. Frey package	A normalized counterexample and its Frey curve	Adapted from the Imperial College London FLT project; `FreyPackage.no_frey_package` is assembled from the four theorems of steps 3 to 6.[4]
3. Irreducibility (Mazur)	The Frey curve's mod p representation is irreducible	For p at least 17, Mazur's Eisenstein-ideal argument (X0(N), its Jacobian and Néron model, the cuspidal subgroup, the Eisenstein quotient), "by far the largest part of the step"; p = 5 by a self-contained descent; p = 7, 11, 13 by Kummer's theorem for regular primes, ported from flt-regular, plus proofs that the rings of integers of the 7th, 11th and 13th cyclotomic fields are principal.[4]
4. Modularity (Wiles)	Every semistable integral Weierstrass model is modular	Langlands-Tunnell in the weight-2 form Wiles uses, two modularity lifting theorems via Taylor-Wiles patching in Diamond's formulation, and the 3-5 switch.[4]
5. Level lowering (Ribet)	A nonzero weight-2 cusp form on Gamma0(2)	Ribet's theorem in the form needed, via Čerednik-Drinfeld uniformization, and the Mazur-Ribet step at p.[4]
6. No cusp forms	S2(Gamma0(2)) = 0	Proved from Mathlib alone.[4]

Buzzard summarized the mathematics in similar terms: the repository develops Fontaine theory to study flat deformations of Galois representations and enough of Mazur's work on the Eisenstein ideal to conclude that no Frey curve can have a point of order p, an argument he read as working only for p at least 17; he added that FLT "was already formalized for odd regular primes" by Best, Birkbeck, Brasca and Rodriguez, that the smallest irregular prime is 37, "so it's all good".[6] PROOF-PATH.md shows that the repository itself closes the small exponents by including a port of the flt-regular argument rather than relying on the external project.[4]

The run, day by day

Anthropic's timeline document counts Day 1 as August 7, 2026, when the run was launched overnight. By Day 2 about 2,100 theorems had been proved on the platform; the proof passed 10,000 theorems on Day 6; and the last open statement closed at 10:00 pm Eastern time on Day 11, August 17, after which "the rest of the proof closes within seconds, running through Ribet's level lowering and the modularity lifting step the proof needs".[2] The post reproduces an agent's reaction from that moment: "The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign."[1] Anthropic notes that other agents treated the platform's "Proved" status as a claim to be checked rather than a result, and that about 25 minutes after the close one agent explained to the project's readers why an independent end-to-end recheck was still needed, since the platform checks each statement on its own.[2]

Day (2026)	Milestone reported by Anthropic
Day 1 (Aug 7)	Run launched overnight; the elementary statement of FLT placed at the top of the tree; existence of the Taylor-Wiles primes proved.[2]
Day 2 (Aug 8)	Order-19 case of Mazur's torsion theorem proved; about 2,100 theorems on the platform; the 3-5 switch proved.[2]
Day 5 (Aug 11)	Irreducibility of the Frey curve's mod p representation (the case of Mazur's theorem the proof needs) marked proved at 9:40 pm ET; the agents' shared plan had that morning estimated the rest of the Mazur argument at "1-3 weeks".[2]
Day 6 (Aug 12)	More than 10,000 theorems proved.[2]
Day 8 (Aug 14)	The central level-switching step in Ribet's argument proved.[2]
Day 9 (Aug 15)	All sixteen Eichler-Shimura steps the proof needs in place, waiting on one open foundational result.[2]
Day 11 (Aug 17)	The needed case of the Langlands-Tunnell theorem proved at 11:05 am ET; the last open statement proved at 10:00 pm ET and FLT marked proved on the platform.[2]
Aug 18-19	All 29,511 cards recompiled from source outside the platform, then the whole tree built as a single Lean project.[2]

The timeline document quotes verbatim excerpts of the agents' reasoning, chosen mostly by Claude, including an agent catching a mistake in another agent's claim about bounded denominators of q-expansions on Day 3, an agent recognizing on Day 4 that a lemma another agent had rated at "days" actually needed Ribet's level lowering, and an agent recalling on Day 5 why the prime 5 needs special care in the Taylor-Wiles argument. Anthropic says it has not independently verified the mathematical claims in those excerpts.[2]

A smaller experiment

Anthropic also reports a smaller experiment in which its researchers used three personal Claude Max subscriptions to formalize applications of the Hardy-Littlewood circle method; collaborating through Prove2Me, the agents completed a formalization of Vinogradov's three-primes theorem in three days. The company says it thinks "collaborative formalization of major results with consumer AI subscriptions is achievable" with the right scaffold.[1]

What exactly was proved

The file Theorems/Thm_fermat_last_theorem.lean declares the statement with Lean's built-in natural numbers:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

The default build target, FinalCheck.lean, contains a #guard_msgs check that the theorem depends on exactly the axioms propext, Classical.choice and Quot.sound, so the build fails if the proof used sorry, an added axiom or native_decide; the same file derives Mathlib's own statement, FermatLastTheorem, from the theorem.[3] The README states that the statement's only Mathlib ingredient is exponentiation on the natural numbers, which Mathlib defines as Lean's built-in exponentiation, and that comparator checks that every definition the statement mentions is identical to stock Mathlib's.[3]

The named classical theorems inside the proof are proved only in the strength the argument needs. PROOF-PATH.md is explicit about this: "Mazur" here is irreducibility of the Frey curve's mod p representation, not Mazur's theorems on rational isogenies or torsion of general curves; "Langlands-Tunnell" is the octahedral case with an explicit lift, not automorphy of general odd two-dimensional representations with soluble image; "Wiles" is modularity of semistable integral Weierstrass models in a trace-matching sense, with nothing said about non-semistable curves, modular parametrizations or L-functions; and "Ribet" is level lowering for the Frey representation as a congruence of traces, not Ribet's theorem for a general modular mod p representation.[4] In an assessment Anthropic solicited from Claude about two weeks after the run, the model quoted the project's internal documentation as saying that none of these restricted versions "should be cited as a formalisation of the general classical theorem".[2]

The README also describes what no tool can check: "that each intermediate theorem means what its name suggests; that is for the reader to judge". The Lean sources were "produced by AI agents building on human-written open-source Lean, with Lean as the arbiter, and are written to be checked rather than read": names are machine-generated, labels such as P2M or hexadecimal suffixes are pipeline labels, comments were removed before release, and "where a name and a statement disagree the statement is what was proved".[3] Anthropic's post adds, in a footnote, that the proof "is likely much longer than it needs to be", which is part of why it dwarfs Mathlib in line count.[1] Claude's own assessment lists further defects: roughly two in five theorem statements inside the proof files repeat a statement made elsewhere, about a fifth of proof-file lines are verbatim copies of declarations found elsewhere in the tree, about 31% of the bytes are generated preambles that switch off instances and simp lemmas, about 11,700 files set their own heartbeat limits, and over 900 files exceed Mathlib's 1,500-line cap.[2]

Verification chain

The repository documents three layers of checking, and Buzzard reports having repeated the first two himself.[3][6]

Check	Tool and version	Result reported in the README
From-scratch build	`lake build` on Lean 4.33.1 (which the README says includes the 2026 kernel soundness fixes), with Mathlib v4.33.0 compiled from source	All 60,475 modules built; every declaration checked by the Lean kernel; axioms exactly `propext`, `Classical.choice`, `Quot.sound`. Anthropic's build took 5 h 32 min at 96 jobs with a peak of 153 GB of memory.[3]
Statement comparison and kernel replay	leanprover/comparator v4.33.0 against `verification/comparator/Challenge.lean`, which states the theorem using only Mathlib	Confirmed the proved statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the whole proof, Mathlib included, replays through the Lean kernel; verdict "Your solution is okay!". About 14 h 46 min, nearly all of it single-core kernel replay, peak memory 230 GB.[3][25]
Independent kernel	nanoda 0.4.13, a Lean kernel reimplementation written in Rust, run on a lean4export dump of the environment	"Checked 1052234 declarations with no errors". The 37.8 GB export takes about an hour and 90 GB of memory; the check about 30 minutes at 16 threads. Anthropic built nanoda with four small patches (one adds progress output, three speed up definitional-equality search) and says none adds, removes or weakens a typing rule.[3][26]

The README further states that no module contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def or #eval, apart from the deliberate sorry in the comparator challenge file, and that together these checks establish that the statement follows from the three axioms "given trust in the Lean kernel (or nanoda) and the checking tools".[3] Anyone repeating the build needs Linux or macOS, about 5 GB of memory per parallel job (a few modules need up to 36 GB), about 67 GB of disk under .lake/ plus about 220 GB of intermediate C files, and a network connection, because no prebuilt Mathlib matches the pinned toolchain.[3]

Buzzard wrote that he compiled the code base and ran comparator on it: "it checks out". He described it as a gigantic proof of over 13.4 million lines that "takes nearly 20 times as long to compile as Lean's mathematics library (on a machine with 96 cores!)", added that Lean was sluggish jumping between files even on a machine with 500 GB of RAM that Anthropic gave him access to, and said the HTML pages Anthropic supplied were easier to explore in practice.[6]

The timeline document records one measure of how brittle the artifact is: when the toolchain was bumped from Lean 4.30 to 4.33 with the matching Mathlib, 7,620 of the 29,511 proof files (26%) changed and 5,672 (19%) needed individual repair, according to Claude's assessment.[2] The attribution file confirms that the tree was assembled on Lean 4.30.0 before the release build.[5]

Repository, attribution and licensing

The repository anthropics/fermats-last-theorem was created on GitHub on September 4, 2026 under the Apache License 2.0, with copyright held by Anthropic, PBC; it describes itself as a "Research artifact. Not maintained and not accepting contributions."[3] The html/ folder, about 390 MB, presents the proof as static web pages: a page for each of the 29,511 theorems (the exact Lean statement, what it cites and what cites it, and an expandable dependency graph) and for each of the 1,450 definition modules, a search box over all names, and a graph of the landmark theorems. The README notes that the English summaries on those pages are generated automatically and that the Lean statement is authoritative.[3]

Because the agents' comments were stripped at release, upstream copyright headers did not survive, and Anthropic reconstructed attribution by comparing every one of the 60,478 .lean files, line by line after normalizing whitespace, against copies of Imperial FLT files that had been brought into its working tree in May 2026 (97 files from the upstream main branch as of May 21, 2026).[5] ATTRIBUTION.md lists 106 files containing material from the Imperial College London FLT project (90 files, covering the Frey package, Galois representations, deformation theory, patching and more) and from flt-regular (Kummer's theorem), with upstream file, copyright holder and author list for each, plus 23 files that reproduce Mathlib text.[3][5] The post's acknowledgments credit Buzzard's project and flt-regular, thank Buzzard for reviewing the proof, and list the mathematicians whose ideas the 1995 proof integrated: Frey, Serre, Ribet, Mazur, Langlands, Tunnell, Taniyama, Shimura and Weil.[1]

Kevin Buzzard's assessment

Anthropic shared the proof with Buzzard before publication and quotes him twice. On the achievement: "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 the implications: "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."[1]

His own blog post the same day, titled "FLT: Anthropic has beaten me to it", is more pointed about what the result does and does not mean. On the mathematics: "Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing."[6] On what it does show: "What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly." He added that machines checking the Langlands program will "ruthlessly flag arguments which are incomplete", that autoformalization "will also keep us honest" about results that papers assume are "known to the experts", and: "This is why I am so excited about the news!"[6]

On his own EPSRC project, Buzzard wrote that "a naive reaction to the news above is that I no longer have any work to do. This is not the case." Anthropic's repository, he said, goes further than what he promised the EPSRC (he undertook only to reduce FLT to 1980s results, while the repository proves the whole theorem), but he also promised pull requests adding fundamental objects of modern number theory to Mathlib, which is ongoing, and "a dynamic document enabling humans to explore the modern proof", which he guessed Anthropic would not produce, since "they did not formalize the modern proof anyway".[6] On cost, he wrote: "I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money".[6] He also recounted that the news first reached him as an email titled "End-to-end Lean formalization of Fermat's Last Theorem" from someone he had never heard of, glimpsed during a moment of phone reception at the Green Man festival in Wales; he "wrote them off as a crank" and only registered the result a week later while clearing nearly 1,000 unread emails.[6]

Claude's own assessment, solicited by Anthropic and reproduced in the timeline document, draws the same contrast from the other side. It describes the Imperial project as "an unfinished library written for people to read, reuse and maintain", built as human-reviewed pull requests to Mathlib's standard along a modern route that avoids Langlands-Tunnell and Ribet and for now assumes 1980s-era inputs, and its own proof as "a finished proof delivered as 60,474 almost entirely machine-written files" that "would fail most of Mathlib's mechanical entry rules". It suggests that the infrastructure the proof built (Hecke algebras, Galois representations of eigenforms, modular curves and their Jacobians, Néron models, finite flat group schemes, Tate curves, deformation rings with Taylor-Wiles patching) could still enter Mathlib "as human-led Mathlib developments that use our files as a worked reference rather than a copy".[2]

Reception

Anthropic announced the result on its Science blog and on X on September 4, 2026, describing the proof as "the largest Lean proof ever written" and "a project experts thought would take many years".[1][7] Buzzard noted that the news technically leaked an hour earlier through an Instagram post by a coffee shop in Islington before Anthropic's official announcement.[6] The Anthropic post reached the front page of Hacker News, where it had about 580 points and about 360 comments by the morning of September 5 UTC; Buzzard's post and the GitHub repository were submitted separately.[29] The GitHub repository had 442 stars and 30 forks as of September 5.[3]

Commenters on Buzzard's blog raised the cost of the run and the length of the output. One reader, responding to the footnote that the proof "is likely much longer than it needs to be", asked: "'Likely'? How about 'definitely'?"[6] Buzzard himself flagged the same tension between what the run cost and what his five-year grant cost, without putting a figure on Anthropic's spend; the company's post gives token counts but no cost figure.[1][6]

Implications

Anthropic's own framing is that verification, not new mathematics, is what is novel here, in contrast to its August 2026 Riemann zeta result, which produced a new theorem.[1][27] The company argues that the speed of the formalization "demonstrates that it is now possible to formalize large swaths of mathematics", which could both catch errors in the existing body of proofs and reduce the burden of refereeing new work; that formalization is "a major factor in how humans can gain confidence in AI-generated mathematical results"; and that "it will become common to produce a formalized proof alongside any write-up intended for a human reader", while a formal proof should not replace a human-readable exposition.[1] Anthropic also reports that writing Lean "seems to help Claude prove novel results", since many of its recent Claude-authored results were formalized in parallel with their proofs, and says it has expanded free and discounted subscriptions and research credits for external researchers, including mathematicians working on formalization, with grants for larger projects that could include formalizing other major theorems.[1]

Buzzard has been pushing the same direction from the mathematical side. In August 2026 his team released a dataset of 50 Lean statements of theorems published in the Annals of Mathematics since 2020, with a challenge for AI systems to autoformalize the proofs from the PDFs; he warned that at least two of the papers rest on 10,000 pages of unformalized group theory and at least one on 2,000 pages of unformalized algebraic geometry.[31] His blog post on the FLT result predicts that on-the-fly formalization of modern research will show "exactly what is being assumed in the proofs of various important results in my field".[6]

The artifact itself is unlikely to be absorbed into Mathlib in its current form. Claude's assessment cites Mathlib's contribution page as listing over 2,600 open pull requests as of mid-2026, its suggestion that fast-moving projects use a standalone repository, and its AI policy requiring contributors to disclose LLM use and to understand all AI-written content.[2] The Imperial project continues on its modern route, with Mathlib pull requests and a human-readable exploration of the proof among its promised outputs, and Buzzard's EPSRC fellowship runs to September 2029.[6][12]

Comparison with other AI mathematics results

Result	Date	System	Nature of the task	Verification
AlphaProof and AlphaGeometry 2 at IMO 2024	July 2024 (Nature paper November 12, 2025)	Google DeepMind, reinforcement learning in Lean	Solving four of six Olympiad problems, 28 of 42 points, silver-medal standard	Formal proofs in Lean.[28][30]
Riemann zeta critical-line bound	August 10, 2026	Anthropic, unreleased research version of Claude, about 60 subagents, 31 million output tokens over two Claude Code sessions	New theorem: raising the proven proportion of zeros on the critical line from 41.6% to 67.2%	Paper reviewed by Anthropic mathematicians and two outside experts; Lean formalization passing comparator.[27]
Vinogradov's three-primes theorem	2026 (reported September 4)	Anthropic researchers on three Claude Max plans, via Prove2Me	Formalizing a known theorem in three days	Lean.[1]
Fermat's Last Theorem	August 7-17, 2026 (published September 4)	Dozens of Claude agents on an internal model, Claude Code harness plus Prove2Me, about 6 billion output tokens	Formalizing an existing 1995 proof end to end	Lean build, comparator, nanoda.[1][2][3]
flt-regular	2021 to 2025	Human authors (Best, Birkbeck, Brasca, Rodriguez Boidi, van de Velde, Yang)	FLT for regular primes	Lean.[17][18]
Imperial College London FLT project	2023 to 2029 (ongoing)	Human contributors led by Buzzard; EPSRC-funded	Modern proof route; initial goal is reduction to 1980s results	Lean, with Mathlib pull requests.[10][11][12]

The FLT formalization differs from AlphaProof-style systems in kind: AlphaProof learns to find proofs of competition problems by reinforcement learning against Lean, whereas the FLT run was autoformalization of a proof that already existed in the literature, orchestrated by general-purpose coding agents. It differs from Anthropic's Riemann zeta result in the opposite direction: that result produced new mathematics with a comparatively small formalization, while the FLT run produced no new mathematics and a very large one.[1][27][28]

By the numbers

Quantity	Value	Source
Duration of the successful run	11 days, August 7-17, 2026	Anthropic[1][2]
Lines of Lean	About 13 million (about 10.5 million without generated boilerplate); Buzzard counts over 13.4 million	Anthropic; Buzzard[2][6]
Theorems used by the final theorem	29,511 (reported as 29,500 in the post)	README; Anthropic[1][3]
Theorems proved on the platform	About 30,300	Anthropic[1][2]
Supporting lemmas local to proof files	About 533,000	Anthropic[2]
Lean modules	60,475	README[3]
Definition modules	1,450	README[3]
Output tokens consumed	About 6 billion	Anthropic[1]
Agents	"Dozens"	Anthropic[1]
Model	Internal research model "roughly comparable to Claude Fable 5.1"	Anthropic[1]
Share of final non-boilerplate lines from failed earlier attempts	About 7%	Anthropic[1]
Size relative to Mathlib	"Over 5x" by lines (Anthropic); "nearly 20 times" the compile time on 96 cores (Buzzard)	Anthropic; Buzzard[1][6]
Toolchain	Lean 4.33.1; Mathlib v4.33.0	README[3]
Axioms	`propext`, `Classical.choice`, `Quot.sound`	README[3]
Build time	5 h 32 min at 96 jobs; peak 153 GB memory	README[3]
comparator run	14 h 46 min; peak 230 GB memory	README[3]
nanoda check	1,052,234 declarations; 37.8 GB export	README[3]
Files adapted from Imperial FLT and flt-regular	106 (90 from Imperial FLT)	README; ATTRIBUTION.md[3][5]
Files reproducing Mathlib text	23	README[3]
Exponents handled by the modular-curve (Mazur) argument	p at least 17; p = 5 by descent; p = 7, 11, 13 by Kummer's theorem; n = 3 and 4 from Mathlib	PROOF-PATH.md; Buzzard[4][6]
Imperial project funding	934,043 pounds, October 2024 to September 2029	UKRI[12]
Imperial blueprint length	86 pages (build of September 4, 2026)	Blueprint PDF[13]
License	Apache-2.0	README; GitHub[3]

Timeline

Date	Event
c. 1637	Fermat writes the claim and his "marvelous proof" note in the margin of Diophantus's Arithmetica.[1]
1908	The Wolfskehl prize of 100,000 gold marks is announced; 621 incorrect proofs arrive in the first year.[1][23]
June 21-23, 1993	Wiles presents his proof in three lectures at the Isaac Newton Institute; a gap is later found.[1][22]
October 24, 1994	Wiles submits the two manuscripts that repair the proof, one co-authored with Taylor.[22]
May 1995	Both papers appear in the Annals of Mathematics, volume 141, issue 3.[20][21]
1995	Darmon, Diamond and Taylor publish their exposition of the proof.[19]
2005	Jan Bergstra proposes formalizing Wiles's proof so that a computer can verify it.[1][22]
October 25, 2021	The flt-regular repository is created.[17]
November 19, 2023	The ImperialCollegeLondon/FLT repository is created; its December 2023 general information page says AI tools cannot yet help much with formalization.[10][11]
October 2024	EPSRC fellowship EP/Y022904/1 begins; Buzzard had said he would devote serious time to the project from then.[11][12]
October 2024	The flt-regular team posts its complete formalization of FLT for regular primes.[18]
December 11, 2024	Buzzard reports on the first two months of the Imperial project.[14]
April 9, 2026	Last modification of Wiedijk's list: 99% formalized, FLT the remaining entry.[16]
May 21, 2026	Anthropic's working tree takes copies of Imperial FLT files, per the attribution file.[5]
July 6-10, 2026	Buzzard's "Formalizing Fermat" workshop in London on AI-assisted formalization of the project's prerequisites.[15]
August 7, 2026	Day 1 of the successful Anthropic run.[2]
August 10, 2026	Anthropic publishes its Riemann zeta result, with a Lean formalization.[27]
August 17, 2026	The last open statement is proved at 10:00 pm ET and FLT is marked proved on Prove2Me (02:00:57 UTC on August 18).[1][2]
August 18-19, 2026	The full tree is recompiled outside the platform and built as a single Lean project.[2]
August 28, 2026	The Prove2Me paper is posted on arXiv.[8]
September 4, 2026	Anthropic publishes the post, the timeline document and the GitHub repository; Buzzard posts his assessment.[1][2][3][6]

References

Formalizing Fermat's Last Theorem - Anthropic, September 4, 2026.
Formalizing Fermat's Last Theorem in Lean: A timeline and selected excerpts from Claude's reasoning - Anthropic (PDF accompanying the September 4, 2026 post).
Fermat's Last Theorem in Lean 4 (README) - GitHub, anthropics/fermats-last-theorem, created September 4, 2026 (metadata fetched September 5, 2026).
PROOF-PATH.md: The route of the proof - GitHub, anthropics/fermats-last-theorem, September 2026.
ATTRIBUTION.md: third-party material in this repository, file by file - GitHub, anthropics/fermats-last-theorem, September 2026.
FLT: Anthropic has beaten me to it - Xena Project (Kevin Buzzard), September 4, 2026, including reader comments by Riccardo Brasca and David Roberts.
Anthropic on X: "Checking that a major mathematical proof is correct can take years..." - @AnthropicAI, September 4, 2026.
Prove2Me: An Open Collaborative Platform for Scaling Math Formalization - arXiv (Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng), August 28, 2026 (v2 August 31, 2026).
Prove2Me: Missions - Prove2Me, accessed September 5, 2026.
ImperialCollegeLondon/FLT: Ongoing Lean formalisation of the proof of Fermat's Last Theorem - GitHub (project README and repository metadata), accessed September 5, 2026.
GENERAL.md: A Lean formalisation of Fermat's Last Theorem - ImperialCollegeLondon/FLT (Kevin Buzzard), December 2023, accessed September 5, 2026.
Formalising Fermat (EP/Y022904/1) - UKRI Gateway to Research, accessed September 5, 2026.
Towards a Lean proof of Fermat's Last Theorem (blueprint) - Imperial College London FLT project (Kevin Buzzard, Richard Taylor), build dated September 4, 2026.
Fermat's Last Theorem - how it's going - Xena Project (Kevin Buzzard), December 11, 2024.
Formalizing Fermat workshop - Xena Project (Kevin Buzzard), May 15, 2026.
Formalizing 100 Theorems - Freek Wiedijk, Radboud University, last modified April 9, 2026.
leanprover-community/flt-regular: Fermat's Last Theorem for regular primes - GitHub, created October 25, 2021, accessed September 5, 2026.
A complete formalization of Fermat's Last Theorem for regular primes in Lean - arXiv (Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van de Velde, Andrew Yang), October 2, 2024; Annals of Formalized Mathematics 1:103-132, 2025.
Fermat's Last Theorem - Henri Darmon, Fred Diamond, Richard Taylor, in Current Developments in Mathematics 1995, International Press, pp. 1-154.
Modular elliptic curves and Fermat's Last Theorem - Annals of Mathematics 141(3): 443-551 (Andrew Wiles), May 1995.
Ring-theoretic properties of certain Hecke algebras - Annals of Mathematics 141(3): 553-572 (Richard Taylor, Andrew Wiles), May 1995.
Wiles's proof of Fermat's Last Theorem - Wikipedia, accessed September 5, 2026.
Fermat's Last Theorem - Wikipedia, accessed September 5, 2026.
Formalizing Fermat's Last Theorem in Lean: A Landmark Mathematical Project - Lean Language (use cases), accessed September 5, 2026.
leanprover/comparator - GitHub, Lean FRO, accessed September 5, 2026.
ammkrn/nanoda_lib: Library implementing type inference/checking functionality based on the Lean theorem prover - GitHub, accessed September 5, 2026.
Learning more about Claude's mathematical capabilities - Anthropic, August 10, 2026 (updated August 13, 2026).
Olympiad-level formal mathematical reasoning with reinforcement learning - Nature 651, 607-613 (Thomas Hubert, Rishi Mehta, Laurent Sartran et al.), November 12, 2025.
Formalizing Fermat's Last Theorem (discussion) - Hacker News, September 4, 2026 (points and comment count as of September 5, 2026).
AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind, July 25, 2024.
The Annals Challenge - Xena Project (Kevin Buzzard), August 13, 2026.

Editing: Formalization of Fermat's Last Theorem (Anthropic, 2026)