Claude formalizes Fermat’s last theorem proof

Anthropic AI said an advanced prototype of Claude turned Fermat’s last theorem into computer-verified code for the first time, producing a 13-million-line-long proof. The company announced the result on 4 September, saying the model finished in 11 days a project that was expected to take humans 10 years.

The achievement marks a significant advance in AI-assisted formalization, the process of translating mathematical arguments into formal code that computers can check. Mathematicians said the Fermat project was far more complex than earlier AI formalization milestones, including work related to Maryna Viazovska’s sphere-packing results in spaces of 8 or 24 dimensions.

Fermat’s last theorem was originally proved in 1994 by Andrew Wiles and Richard Taylor, more than 350 years after Pierre de Fermat made the claim in 1637. Researchers quoted in the report said the result suggests AI could increasingly help verify mathematical work and may eventually scrutinize large parts of the existing mathematical literature.