Anthropic researchers announced that Claude produced the first complete, computer-verified proof of Fermat’s Last Theorem in the Lean proof assistant, working largely autonomously over 11 days and generating 13 million lines of Lean code. The system proved roughly 29,500 intermediate theorems on the path to formalizing Andrew Wiles’s 1995 proof, a task mathematicians had expected to take years. Mathematician Kevin Buzzard called it a “big step towards automatic formalization of the modern mathematical literature.”
