Anthropic Releases Lean Proof of Fermat's Last Theorem

Anthropic posted that its model Claude turned Andrew Wiles' 1995 proof of Fermat's Last Theorem into a Lean formalization spanning 13 million lines and 29,500 intermediate theorems. The company called it the largest Lean proof constructed and published the code on GitHub. The Lean account and several researchers shared the announcement. Replies on X noted the scale compared to Mathlib and asked about verification limits. Other posts highlighted that the work converts an existing human proof rather than generating a new one.