AI company Anthropic has created a formalised proof of Fermat鈥檚 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鈥檚 last theorem puzzled mathematicians for centuries until it聽was proved 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.
Advertisement
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, which 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.
Earlier this year, a conference of AI experts, computer scientists and mathematicians was held in London by 聽at Imperial College London, who was 鈥� until Anthropic鈥檚 announcement 鈥� working on a聽five-year project聽to formalise Wiles and Taylor鈥檚 100-page proof in a programming language called Lean, so that it can be formally checked for correctness and used as a foundation for further research.
Buzzard said at the time that when his project began he was confident of success, but that recent advances in AI had convinced him that the project would be complete much faster than he previously thought possible. Anthropic鈥檚 has now overtaken that effort and wrapped up the problem.
Buzzard said in a statement published by Anthropic that the company鈥檚 proof leaves 鈥渘o assumptions other than the axioms of mathematics鈥�. In short, the problem is solved.
鈥淎long the way we see autoformalisation of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalisation artefacts are now robust enough to be built upon; the proof is multi-layered,鈥� said Buzzard. 鈥淚f the automatic formalisation of FLT is possible now, then we have taken a big step towards automatic formalisation of the modern mathematical literature.鈥�
In its blog post announcing the result, Anthropic wrote that its Claude model worked continuously and autonomously for 11 days to write the proof. Numerous separate AI agents were involved, with different tasks, like tackling smaller chunks of the theorem, being assigned to each.
Human experts occasionally issued 鈥渉igh-level instructions鈥� to keep the work on track, the company says. Several times, the agents 鈥渓ost track of the project鈥檚 state and stopped collaborating effectively鈥�. Interestingly, the company said that success came after it began using a tool designed for human mathematical collaboration called Prove2Me, which helped different agents track their work and decide on next tasks.
Anthropic鈥檚 formalisation runs to 13 million lines of Lean and covers roughly 29,500 intermediate theorems that were necessary stepping stones towards completing the overall work. That makes the proof over five times the current size of all previous work on Mathlib, which also makes it the largest Lean proof ever written.
