Claude formalizes Fermat's Last Theorem

Anthropic says Claude completed the first complete computer-checked formalization of Fermat’s Last Theorem in 11 days, writing 13 million lines of Lean and proving 29,500 intermediate theorems, according to its research report on the formalization. Lean checked the finished proof against its three standard axioms; Anthropic says dozens of agents collaborated through Prove2Me and consumed about six billion output tokens. The result is a verification milestone rather than a new mathematical discovery, so teams building AI research systems should budget for theorem graphs and machine-checked artifacts—not treat model prose as the deliverable—alongside recent AI-generated mathematics work.