Anthropic Claims Claude Formalized FLT in 11 Days; Dispute Follows

Anthropic announced that Claude completed a machine-verified formalization of Fermat's Last Theorem in 11 days, producing over 13 million lines of Lean code. Dozens of Claude agents converted the Andrew Wiles-based proof into machine-checkable code, with agents cross-checking each other's work during the run. Anthropic called the result the largest Lean proof ever written and said it proves over 29,000 supporting theorems across areas of mathematics never previously formalized. A dev.to article disputes the claim, stating that the Lean formalization of FLT is an ongoing community-led effort and arguing that what Claude completed covers only FLT for regular primes, a special case, not the general theorem.