Claude formalizes for the first time an integral proof of Fermat's last theorem

In 11 days, largely autonomously, the model produced 13 million lines of Lean code and proved more than 30,000 intermediate theorems.

Anthropic announces that his model Claude produced the first fully computer-checked demonstration of Fermat's latest theorem, written in Lean's formal proof language. The exercise mobilized several agents Claude for 11 days, for a total of about six billion tokens generated, 13 million lines of code and over 30,300 demonstrated intermediate theorems, including 29 500 actually used in the final proof.

The breakthrough came from the use of Prove2Me, an open source collaborative platform designed by researcher Anthropic Tianyi Peng and his Columbia University team, which organizes a graph of statements to be demonstrated and coordinates several AI agents around this graph. Kevin Buzzard, mathematician at Imperial College London, who has been piloting a community effort to formalize the same theorem for years, has reviewed and validated the artifact produced.