Mathematician Andrew Wiles completed the proof to Fermat’s last theorem in 1994, more than 350 years after Pierre Fermat proposed the conjecture.Credit: AP Photo/Charles Rex Arbogast/Alamy Fermat’s last theorem, one of the most celebrated mathematical results of the last half-century, has been turned into computer-verified code for the first time, using an advanced prototype of
Mathematician Andrew Wiles completed the proof to Fermat’s last theorem in 1994, more than 350 years after Pierre Fermat proposed the conjecture.Credit: AP Photo/Charles Rex Arbogast/Alamy
Fermat’s last theorem, one of the most celebrated mathematical results of the last half-century, has been turned into computer-verified code for the first time, using an advanced prototype of the artificial-intelligence (AI) chatbot Claude.
AI cracks 80-year-old mathematics challenge — researchers are astonished
The fact that a machine could turn the work of human mathematicians into a 13-million-line-long, ironclad proof “just completely blew my mind”, says Alex Kontorovich, a number theorist at Rutgers University in Piscataway, New Jersey. Claude-maker Anthropic AI, of San Francisco, California, announced the breakthrough on 4 September. The model finished in 11 days a project that was expected to take humans 10 years.
The result shows that AI will play an increasingly important part in checking the work of mathematicians — as well as in producing new mathematical reasoning. At the current pace of progress, it is not unthinkable that AI could soon be able to scrutinize the entire library of mathematical knowledge, perhaps finding that some well-known results are wrong. “Two years ago, that was a fantasy,” says Kevin Buzzard, a mathematician at Imperial College London.
Mathematicians astounded
Mathematicians have been increasingly astounded by the pace at which AI’s mathematical skill have soared. This includes the technology’s ability to ‘formalize’ proofs — translating mathematical arguments from natural language into a formal, computer-certifiable code, typically in the programming language Lean.
In February, AI achieved another milestone in AI-aided ‘formalization’, when it certified the Fields-medal-winning work on the most efficient ways to pack spheres (in a space of 8 or 24 dimensions) of Maryna Viazovska. But Buzzard says that the Fermat’s last theorem work was on a whole other level of complexity. “It was maybe an order of magnitude more difficult,” he says.
Daniel Litt, a number theorist at the University of Toronto, Canada, agrees. “If they can formalize Fermat’s last theorem, they can probably formalize anything.”
‘It is incredible’: How AI is transforming mathematics
The original proof of Fermat’s last theorem, completed in 1994 by Andrew Wiles and Richard Taylor, was a landmark result of twentieth-century mathematics. The deceptively simple statement is that there cannot be any whole numbers x, y and z such that xn + yn = zn, if n is greater than 2. French mathematician Pierre de Fermat had made this claim in 1637 but did not leave behind a proof, and it became known as ‘his’ last theorem — even though in mathematics, a statement earns the ‘theorem’ badge only after it has been rigorously proven to be true.
(By itself, solving this particular equation — or knowing that it has no solutions — does not have much practical use, but the techniques Wiles developed to crack the problem helped to bring distant disciplines of mathematics together. The proof earned Wiles an Abel Prize, one of the most coveted awards in mathematics, in 2016.)
Check back often for more exciting news!
