In 1637, the mathematician Pierre de Fermat proposed a statement regarding the equation $x^n + y^n = z^n$, where $x$, $y$, $z$, and $n$ are positive integers. Fermat claimed that there would be no valid solution to this equation if the exponent $n$ was greater than 2.
This means there is no combination of values for $x$, $y$, and $z$ that makes the statement true; according to Fermat, the sum of $x^n$ with $y^n$ would never result in $z^n$. The necessity for $n$ to be greater than 2 can be contrasted with the Pythagorean Theorem ($x^2 + y^2 = z^2$), which is true, as exemplified by $3^2 + 4^2 = 5^2$, proving that Fermat's negation does not apply when $n=2$.
Fermat postulated that the impossibility of solutions persisted for $n=3$, $n=4$, and other larger values, but he never recorded the proof he had in mind. This concept is known as Fermat's Last Theorem. It took 357 years for someone to prove Fermat's correctness, with Andrew Wiles concluding the proof in 1994, an event considered a scientific milestone of the 20th century. For this achievement, Wiles received the Abel Prize in 2016.
Recently, a prototype of the Claude artificial intelligence model transformed this demonstration into verifiable code consisting of 13 million lines. Anthropic, the developer of Claude, released this announcement on September 4. The AI took only 11 days to complete the project, while it is estimated that humans would take about 10 years to perform the same work.
It is important to note that Claude did not solve the problem, but rather formalized its proof. It converted a demonstration originally written in natural language (words) into a formal proof capable of computational verification, essentially translating the human argument into the logical language of machines using the open-source programming language Lean.
This formalization contributes to the growing body of advancements of AIs in mathematics, either by assisting human researchers or generating new reasoning. Kevin Buzzard, a mathematician at Imperial College London, commented in an interview with Nature that such capability was considered fiction just two years ago. Researcher Buzzard has been working on the formalization of Fermat's Theorem in Lean since 2024.
To formalize a mathematical demonstration in Lean, the system must know prior concepts, arguments, and proofs, as mathematical knowledge is built upon already validated assertions. To handle increasingly complex proofs, mathematicians have developed Mathlib, a library of formalizations in Lean, whose inclusions are subject to curation by human experts.
Previously, the review of mathematical demonstrations depended exclusively on human experts dedicating years to verifying the logical chain of arguments. However, many proofs are published in less visible journals, limiting their reach and leaving their validity uncertain, which hinders progress in certain areas of mathematics that depend on them. Many mathematicians hope that the combination of AI formalization with Mathlib and human checking can optimize the work of scientific journal reviewers and drive mathematical advancement.