Mathematician Andrew Wiles completed the proof of Fermat’s Last Theorem in 1994, more than 350 years after Pierre Fermat first proposed the conjecture.Credit: AP Photo/Charles Rex Arbogast/Alamy
Fermat’s Last Theorem, one of the most famous results in modern mathematics, has been converted into computer-verified code for the first time. The project used an advanced prototype of Anthropic’s artificial-intelligence (AI) chatbot, Claude.
AI cracks 80-year-old mathematics challenge — researchers are astonished
Claude transformed the work of human mathematicians into a rigorous proof consisting of 13 million lines of code. The achievement “just completely blew my mind,” says Alex Kontorovich, a number theorist at Rutgers University in Piscataway, New Jersey. Anthropic, the San Francisco-based company behind Claude, announced the breakthrough on 4 September. The AI model completed the project in 11 days, compared with an estimated 10 years of work for human researchers.
The result highlights the growing role of AI in mathematics, both as a tool for checking established proofs and as a possible aid to discovering new mathematical ideas. If current progress continues, AI could eventually examine large parts of the mathematical literature and potentially identify errors in results long thought to be correct. “Two years ago, that was a fantasy,” says Kevin Buzzard, a mathematician at Imperial College London.
Mathematicians are astounded by AI’s progress
Researchers have been increasingly impressed by the rapid improvement of AI systems in mathematical reasoning. One important capability is formalization: translating mathematical arguments written in natural language into formal code that can be checked by a computer, often using the Lean programming language.
AI reached another major formalization milestone in February, when it helped certify the Fields Medal-winning work of Maryna Viazovska on the most efficient ways to pack spheres in eight- or 24-dimensional space. But Buzzard says that formalizing Fermat’s Last Theorem was far more difficult. “It was maybe an order of magnitude more difficult,” he says.
Daniel Litt, a number theorist at the University of Toronto in 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 was completed in 1994 by Andrew Wiles, with important contributions from Richard Taylor. It became one of the defining achievements of twentieth-century mathematics. The theorem states that there are no positive whole numbers x, y and z that satisfy xn + yn = zn when n is greater than 2.
French mathematician Pierre de Fermat proposed the claim in 1637 but did not provide a proof. It became known as Fermat’s “last theorem”, although a mathematical statement is formally called a theorem only after it has been rigorously proven.
Fermat’s equation has limited direct practical use. However, the mathematical techniques developed by Wiles to solve the problem connected previously distant areas of mathematics. His achievement was recognized with the Abel Prize, one of the highest honors in mathematics, in 2016.
Source: www.nature.com