Overview
- Anthropic published a GitHub repository saying its Claude model produced a complete Lean 4 formalization of Fermat’s Last Theorem with about 29,511 theorems and 1,450 definitions.
- Lean community reporting and the public Imperial College project led by Kevin Buzzard say the FLT formalization is an ongoing, community-led effort and warn the Claude attribution overstates the case.
- A 2025 arXiv paper by Best and colleagues formalized the regular-prime special case of FLT in Lean, showing parts of the theorem were already formalized before Anthropic’s disclosure.
- Experts note the claimed result builds on extensive human scaffolding and shared libraries such as Mathlib, so kernel-level verification and a clear log of human versus AI contributions are required.
- The episode tests how AI tools can speed formal proof work and highlights the need for standards on independent checking, authorship, and integration of AI outputs into high-assurance workflows.