tl;dr: Anthropic used Claude to autonomously produce the first complete, computer-verified proof of Fermat's Last Theorem in Lean, taking 11 days and generating 13 million lines of code across 29,500 intermediate theorems. The effort followed Wiles's proof (via the Darmon-Diamond-Taylor exposition) and succeeded after switching to Prove2Me, a collaborative platform that coordinated multiple agents via a DAG of theorem statements. Kevin Buzzard reviewed the proof and suggested it signals a major step toward automated formalization of modern mathematics, potentially reducing referee burden and catching errors in the existing corpus.