Vintage: 2026-09. Primary evidence is Anthropic's Sep 4, 2026 Science Blog plus the fetched anthropics/fermats-last-theorem README, as hydrated in 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean. Official @AnthropicAI X matches those text claims. The announce post has a video attachment that was not transcribed (x_video: true); claims here are from the post's note_tweet text, the blog, and the README — do not treat video demos as grain. Kevin Buzzard quotes are Anthropic-reported, not an independent Buzzard primary. This is autoformalization / verification of a known proof path, not a new human-readable proof of Fermat's Last Theorem.

Claude formalizes Fermat's Last Theorem in Lean (Anthropic, Sep 4, 2026)

One-line summary: Anthropic says Claude produced the first end-to-end, computer-checked Lean proof of Fermat's Last Theorem in 11 days (~13 million lines; ~29,500–30,300 intermediate theorems) via prove2me plus a claude-code multi-agent harness — checking a Darmon–Diamond–Taylor / Wiles / Taylor–Wiles path, not inventing a new proof of FLT.

The insight

This is a dated lab primary on verification / autoformalization, not on novel mathematics. Anthropic explicitly contrasts the artifact with Claude's recent Riemann-adjacent novel work. Human mathematical input is described as occasional high-level steering from Anthropic researcher Tianyi Peng. Success is attributed to switching to prove2me (DAG of theorem statements, statement/proof file separation, natural-language search/reuse) plus a Claude Code multi-agent harness. Token spend is about six billion output tokens from a general-purpose internal research model "roughly comparable to claude-fable-5-1."

Do not file this as "Claude proved FLT" in the human-conjecture sense. Do not collapse it into the separate, ongoing Imperial College London FLT Lean project.

It is a mid-2026+ instance of the verifiable-layer spike on ai-math-capability-jaggedness (tight Lean check of a known path). It is not a definition- or conjecture-generator result and does not close can-llms-choose-the-right-research-question.

Evidence

All bullets are from 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean (method: grok-bot; fetch_method: x-mcp + webfetch). Permalinks and issuer URLs live on the source page.

Sep 4 issuer claim

• From 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean (Formalizing Fermat's Last Theorem, Sep 4, 2026): Claude worked largely autonomously for 11 days, wrote 13 million lines of Lean, and proved 29,500 intermediate theorems used in the final proof (blog also says 30,300 theorems proved along the way).
• From the same source (same blog): human mathematical input is occasional high-level steering from Anthropic researcher Tianyi Peng. The argument follows a simplified Darmon–Diamond–Taylor exposition of the Wiles / Taylor–Wiles route.
• From the same source (same blog): Anthropic quotes Kevin Buzzard calling it an "extraordinary autoformalization achievement" that proves FLT "with no assumptions other than the axioms of mathematics" and saying the artefacts are "robust enough to be built upon." Treat those quotes as Anthropic-reported, not as an independent Buzzard primary fetched this pass.
• From the same source (@AnthropicAI, 2026-09-04): same-day X restates formalized FLT; largest Lean proof; 13M+ lines; 29,000+ other theorems; links the blog plus GitHub. Video attachment not transcribed — post text only.

GitHub artifact — statement, axioms, verification

• From the same source (anthropics/fermats-last-theorem README, fetched 2026-09-04): Lean statement fermat_last_theorem for n ≥ 3 and positive naturals; #print axioms guard requiring exactly Lean's three standard axioms (propext, Classical.choice, Quot.sound).
• From the same source (same README): from-scratch lake build on Lean 4.33.1 with Mathlib v4.33.0; comparator verdict "Your solution is okay!"; independent Rust kernel (nanoda 0.4.13) accepting an export ("Checked 1052234 declarations with no errors"); three Anthropic speed patches that the README says do not change typing rules.
• From the same source (same README): offline html/ browse of the proof names 29,511 theorems — same order of magnitude as the blog's 29,500 / 30,300; do not flatten the slight count differences into one exact number.
• From the same source (same README): Apache-2.0; credits Imperial College London FLT and flt-regular material in named files. Research artifact: "Not maintained and not accepting contributions."

Harness

• From the same source (blog): success attributed to switching to prove2me plus a claude-code multi-agent harness. Token spend about six billion output tokens from a general-purpose internal research model "roughly comparable to Claude Fable 5.1." Early failed runs without Prove2Me contributed ~7% of non-boilerplate lines. Scaffolding paper: Prove2Me: An open collaborative platform for scaling math formalization (Chen, Marwaha, Lu, Yuen, Peng; arXiv:2608.28433).
• From the same source (blog): a smaller consumer-Max experiment (Vinogradov's Three Primes via the Hardy–Littlewood Circle Method in three days) is a related anecdote, not the FLT claim.

Do not conflate with Imperial FLT

• From the same source: the community Imperial College London FLT / Lean community announcement and mid-2026 workshop coverage (e.g. New Scientist on AI assisting Buzzard's formalization) are a separate, ongoing human-led formalization. Anthropic's Sep 4 artifact adapts pieces from that lineage and quotes Buzzard after review; this clip does not close or replace the Imperial project timeline.

What this source does not establish

• Not a new proof of FLT. Autoformalization of an existing human proof path.
• Not an independent Buzzard primary. Quotes live on Anthropic's page only.
• Video not transcribed. @AnthropicAI announce is silent video (no audio stream); do not cite video-only demo claims.
• Theorem counts are issuer-reported ranges, not one reconciled number (blog 29,500 used / 30,300 along the way vs README html 29,511).
• Kernel trust is still Lean (or patched nanoda) plus a human semantic audit that intermediate theorem names match intended math — Anthropic and Buzzard both flag that.
• Not a rewrite of automated-alignment-researchers, claude-de-novo-protein-binders, or claude-fable-5-1.
• Not promoted here: same-window @GeminiApp Daily Brief and @AIatMeta Muse Spark 1.3 max.
• No person pages for Tianyi Peng or Kevin Buzzard — one steering mention and Anthropic-reported quotes.
• No ticker, 8-K, or stock-market tag.
• Not a rewrite by the Sep 8 Buckmaster–Alpöge forced-blowup clip. Different theorem, different authors. Chronological neighbor only: buckmaster-alpoge-forced-blowups. From 2026-09-08-x-morning-buckmaster-alpoge-ai-fluid-proofs-openai-credit.

Contradictions / tensions

• Novel math vs verification: Anthropic contrasts this with recent Riemann-adjacent novel work. Keep the split.
• Theorem counts: 29,500 / 30,300 / 29,511 — same campaign, slightly different tallies. Not reconciled.
• Buzzard endorsement: Anthropic-reported; no independent primary this pass.
• Imperial vs Anthropic artifact: separate timelines; Anthropic adapts named files and quotes Buzzard after review. Not collapsed.

Open questions

• Does an independent mathematician or Lean FRO audit dispute the statement match, axiom set, or verification claims?
• What does an independent Buzzard primary (if fetched) add or narrow versus the Anthropic-page quotes?
• Does the silent announce video show anything the blog / README / note_tweet do not? Held until transcribed.
• How does this artifact sit next to the still-open Imperial FLT project timeline?

Sources

• 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean

Related

• prove2me
• anthropic
• claude-code
• claude-fable-5-1
• agent-harness
• ai-math-capability-jaggedness
• mathematics-in-the-age-of-ai
• math-verification-loop-to-jagged-ai-progress
• automated-ai-research-llm-capability-boundary
• can-llms-choose-the-right-research-question — status stays open; do not close as yes
• automated-alignment-researchers
• grant-sanderson
• buckmaster-alpoge-forced-blowups — Sep 8 forced Euler/Boussinesq/IPM Lean results; do not collapse into FLT