Fermat's Last Theorem: Claude formalises it in 11 days

Last July, a Nobel laureate in physics had recounted getting help from the artificial intelligence Claude to solve a physics problem. Anthropic has now announced that an experimental Claude model formalised the proof of Fermat's Last Theorem in the Lean language in eleven days. The work consists of translating a complex mathematical proof into code that a computer can check step by step.

To reach this result, Claude generated around 13 million lines of code and 30,300 intermediate theorems. The comparison with human effort gives a sense of the scale of the achievement: the project led by mathematician Kevin Buzzard to fully formalise the theorem had been estimated to take around ten years.

Fermat's Last Theorem was formulated in 1637 by Pierre de Fermat. It states that, for every integer n greater than 2, the equation xⁿ + yⁿ = zⁿ has no positive nonzero integer solutions. The problem remained unsolved for more than three centuries, until Andrew Wiles proved it in the 1990s, with a contribution from Richard Taylor.

What Claude actually did

The work of the artificial intelligence does not consist in having found a new proof: Wiles's proof remains valid and has not been called into question. Instead, Claude turned the existing proof into a formal sequence of steps that a computer can check. That is precisely the purpose of Lean, the language and environment used to formalise mathematics.

The result does have a limitation. The code produced by the artificial intelligence cannot yet be integrated into Mathlib, the standard library used by the scientific community for formal mathematics. The formalisation is therefore complete, but not yet ready to enter the shared ecosystem of mathematicians on a stable basis.

The experiment nonetheless points to a promising direction for artificial intelligence applied to mathematics: not simply generating answers, but building formally verifiable proofs. According to the announcement, the next challenge will be to make such results not only fast to obtain, but also readable and reusable by mathematicians.