Fermat’s last theorem formalised by AI agents in just 11 days

AI company Anthropic has created a formalised proof of Fermat’s last theorem. It took just 11 days for a group of AI agents to complete the task, confirming that the human-found proof proposed in the 1990s is correct.

Fermat’s last theorem puzzled mathematicians for centuries until it was proven in 1995 by Andrew Wiles. It states that there are no whole numbers a, b, and c that satisfy the equation aⁿ + bⁿ = cⁿ, where n is a whole number greater than 2.

The theorem though easy to state was fiendishly difficult to prove. Mathematician Pierre de Fermat posed the puzzle in the 17th century and famously alluded to a proof that he claimed to have discovered, saying that it was too large to fit in the margins of the textbook he was writing in.

Many mathematicians tried and failed to find a proof. Wiles worked on the problem for seven years in secret before announcing his breakthrough in 1993. Proofs often involve lengthy logical arguments that build on each other. If a single step contains an error then the whole thing can collapse. This happened to Wiles when a flaw was found in his proof that took him and collaborator Richard Taylor around a year to fix.

Formalising mathematical theorems is a solution to this problem. It takes them out of the realm of pen and paper, and puts them into a configuration – computer code – that allows machines to grapple with them, methodically working through the logic and exposing any flaws. There are already 2 million lines of formalised mathematics stored in a central repository called Mathlib.