Issue 30Published September 5, 2026
Editor noteThis archived Ash AI Daily issue retains the delivered editorial briefing and final cards.
Story 1AI Daily
Anthropic releases a Lean-checked formalization of Fermat’s Last Theorem
Anthropic says Claude agents produced a complete formalization of Fermat’s Last Theorem in Lean over 11 days. The company reports 13 million lines of Lean code and 29,500 intermediate theorems used in the final proof. Lean checked the proof using its three standard axioms; Anthropic also published the code and a comparator check. Evidence maturity: company research report with a mechanically checked artifact; not peer-reviewed or independently replicated as an AI-method result.
- Anthropic says Claude agents produced a complete formalization of Fermat’s Last Theorem in Lean over 11 days. The company reports 13 million lines of Lean code and 29,500 intermediate theorems used in the final proof. Lean checked the proof using its three standard axioms; Anthropic also published the code and a comparator check. Evidence maturity: company research report with a mechanically checked artifact; not peer-reviewed or independently replicated as an AI-method result.
Why it matters
Formalization turns mathematical reasoning into code a proof assistant can mechanically check. That could reduce verification bottlenecks as AI systems generate more mathematical work, but this demonstration is not evidence that autonomous research is generally reliable.
Sources
Anthropic releases a Lean-checked formalization of Fermat’s Last TheoremAnthropic — Formalizing Fermat’s Last Theorem · Sep 5, 2026
