Overview
- Anthropic announced on Sunday that dozens of Claude agents produced a Lean formalization of Fermat’s Last Theorem in eleven days, yielding roughly 13 million lines of code and about 29,500 intermediate theorems.
- The work was written against Lean and Mathlib and published on GitHub with a written walk-through so anyone can compile the artifacts and check the proof against Lean’s core rules.
- Anthropic credits the result to orchestration and tooling—specifically the Prove2Me platform—while saying human input was limited to occasional high-level guidance from researchers.
- Imperial College’s Kevin Buzzard compiled the repository, ran a comparator and reported the formalization 'holds up,' but wider community review and deeper vetting remain ongoing.
- The effort verifies an existing 1990s proof rather than creating new mathematics and raises open questions about cost (an estimated $100k–$300k), code size, maintainability, provenance, and standards for independent verification.