Claude turns Fermat’s Last Theorem into machine-checkable Lean code
Claude spent 11 largely autonomous days translating Fermat’s Last Theorem into Lean, producing 13 million lines of code and 29,500 intermediate theorems. The result is a complete computer-checked formalization of Wiles’s 1995 proof, not a new proof of the theorem itself. That distinction matters: formalizing difficult mathematics could shrink the years-long gap between a result being announced and every logical step being independently checked.