Claude formalizes Fermat's Last Theorem in Lean — on Mathlib and Prove2Me
Every URL the pipeline pulled into ranking for this issue — primary sources plus the supporting and contradicting findings each Researcher returned. Inline citations in the issue point back here.
Sources
Formalizing Fermat’s Last Theorem anthropic.com
References
dev.to (alifar) — ‘The community project and Claude’s real role’ dev.to
Anthropic’s repository credits 106 upstream files to the existing community FLT project at Imperial College London and to Mathlib, undercutting the ‘fully autonomous’ framing in press coverage.
Techstrong.ai techstrong.ai
Kevin Buzzard called it an ‘extraordinary autoformalization achievement’ but noted Claude followed the 1995 Darmon–Diamond–Taylor exposition of Wiles, not the modern Khare–Taylor proof his own EPSRC-funded project is targeting — so the human effort remains ‘essential’.
dev.to (jamilxt) — ‘AI agents failed… then they got a shared to-do list’ dev.to
Early Claude attempts failed as agents ‘lost track of state and trampled each other’s work’; success only came after Prove2Me externalized state into a shared DAG acting as collective memory for dozens of parallel agents.
36Kr (EN) eu.36kr.com
At retail API rates the six billion output tokens represent roughly $300,000 of compute; with a ~70% gross margin the true cost to Anthropic is closer to $100,000 — versus the £1M-scale multi-year grants awarded for human formalization projects.
ExplainX analysis explainx.ai
The 13M-line artifact is roughly five times Mathlib and contains an estimated 2.5 million lines of repetitive boilerplate; critics call it ‘write-only’ code that swaps one verification problem (peer review) for another (auditing AI-generated codebases).
AIWeekly aiweekly.co
As a secondary benchmark, three Claude agents formalized Vinogradov’s Three Primes Theorem in three days using consumer-tier Claude Max subscriptions — suggesting the barrier to entry for serious formalization may collapse to a $90/month plan.
