Anthropic: Claude formalizes Fermat's Last Theorem in Lean

Generated by Grok Bot research on 2026-09-04. Built-in WebSearch/WebFetch + native X (no Parallel). Treat as raw material — review before promoting into a project or thread.

Summary

After the morning/afternoon AI-thread X clips (Omen / Unsloth overnight; Lyria 3.5 Gemini access), the high-signal frontier-lab original on the 3pm ET pull was Anthropic research, not a new foundation-model card. Verified @AnthropicAI (2026-09-04 18:50 UTC) announced that Claude completed the first formalized proof of Fermat's Last Theorem in Lean; the matching issuer page, dated Sep 4, 2026, is Formalizing Fermat's Last Theorem. The X post has a video attachment (not transcribed); load-bearing claims below are from the post's note_tweet text, the Science Blog, and the GitHub README. This is verification / autoformalization of a known proof path, not a new human-readable proof of FLT.

Findings

Sep 4 Anthropic claim: first end-to-end Lean-checked FLT

Anthropic's Science Blog (fetched 2026-09-04) states 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). Human mathematical input is described as occasional high-level steering from Anthropic researcher Tianyi Peng. The argument follows a simplified Darmon–Diamond–Taylor exposition of the Wiles / Taylor–Wiles route. 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 we fetched.

The same-day X announce restates the headline (formalized FLT; largest Lean proof; 13M+ lines; 29,000+ other theorems) and links the blog plus GitHub. Because the post is video-backed, do not promote any video-only demo claims until transcribed.

GitHub artifact: statement, axioms, and verification story

The public repo anthropics/fermats-last-theorem README (fetched 2026-09-04) gives the Lean statement fermat_last_theorem for n ≥ 3 and positive naturals, and a #print axioms guard requiring exactly Lean's three standard axioms (propext, Classical.choice, Quot.sound). It claims a from-scratch lake build on Lean 4.33.1 with Mathlib v4.33.0, comparator verdict "Your solution is okay!", and an independent Rust kernel (nanoda 0.4.13) accepting an export ("Checked 1052234 declarations with no errors"), with three Anthropic speed patches that the README says do not change typing rules. The offline html/ browse of the proof names 29,511 theorems — same order of magnitude as the blog's 29,500 / 30,300 figures; do not flatten the slight count differences into one exact number.

Licence is Apache-2.0; README credits Imperial College London FLT and flt-regular material in named files. Research artifact: "Not maintained and not accepting contributions."

Harness: Prove2Me + multi-agent Claude Code

The blog attributes success 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 stated as about six billion output tokens from a general-purpose internal research model "roughly comparable to Claude Fable 5.1." Early failed runs without Prove2Me are said to have contributed ~7% of non-boilerplate lines. Scaffolding paper cited on the blog: Prove2Me: An open collaborative platform for scaling math formalization (Chen, Marwaha, Lu, Yuen, Peng; arXiv:2608.28433).

A smaller consumer-Max experiment on the same blog (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 the Imperial multi-year FLT Lean project

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, but this clip does not close or replace the Imperial project timeline.

Other afternoon lab posts (not promoted here)

Same window also saw @GeminiApp Daily Brief free expansion in the U.S. and @AIatMeta Muse Spark 1.3 max (quoting @alexandr_wang). Left out of this clip to keep one topic; Lyria 3.5 Gemini posts from earlier today are already in the AI-thread Lyria source.

Contradictions and open questions

• Novel math vs verification: Anthropic explicitly contrasts this with Claude's recent Riemann-adjacent novel work — FLT here is checking / formalizing an existing proof path. Do not file as "Claude proved FLT" in the human-conjecture sense.
• Theorem counts: blog 29,500 used / 30,300 along the way vs README html 29,511 — same campaign, slightly different tallies; keep as issuer-reported ranges.
• Buzzard endorsement: quoted on Anthropic's page; no independent Buzzard primary fetched this pass.
• Kernel trust: README's verification story still trusts Lean (or patched nanoda) and that intermediate theorem names match intended math — Anthropic and Buzzard both flag that semantic audit remains human.
• Video: @AnthropicAI announce video not transcribed.
• Gemini 4 "PREDICTED" benchmark cluster in afternoon X news was unverified prediction chatter — not grain; skipped.

Provenance

Method: Grok Bot / WebSearch + WebFetch / native X (search_news as post-id pointers only; get_users_by_usernames + get_users_posts on lab accounts; skipped search_posts_all on user-OAuth) Generated: 2026-09-04 fetch_method: x-mcp + webfetch Window: posts newer than same-day AI-thread X clips (overnight Omen/Unsloth; Lyria 3.5 access); lab timelines from start_time 2026-09-04T14:00:00Z; news clusters not cited as grain

Web sources:

• Formalizing Fermat's Last Theorem (Anthropic Science) — Sep 4, 2026 issuer claim; 11 days; 13M lines; theorem counts; Prove2Me; Buzzard quotes; token spend
• anthropics/fermats-last-theorem README — Lean statement; three-axiom guard; Lean 4.33.1 / Mathlib v4.33.0; comparator + nanoda; 29,511 html theorems; Apache-2.0
• Prove2Me arXiv:2608.28433 — platform scaffolding paper (Chen et al.)
• Lean community FLT announcement — separate Imperial multi-year project context
• New Scientist: AI on Fermat formalization workshop — mid-2026 workshop context; not today's Anthropic drop

X sources:

• X post by @AnthropicAI (2026-09-04) — FLT Lean formalization announce; blog + GitHub links (video not transcribed)
• X post by @GeminiApp (2026-09-04) — Daily Brief free U.S. expansion (noted, not promoted)
• X post by @AIatMeta (2026-09-04) — Muse Spark 1.3 max pointer (noted, not promoted)

Grokipedia:

• not used