Fermat's Last Theorem

The question

Around 1637 the French lawyer and mathematician Pierre de Fermat was reading an ancient Greek book on arithmetic. Next to a problem about squares, he wrote in the margin that the equation xⁿ + yⁿ = zⁿ has no solutions in positive whole numbers for any n greater than 2. For squares there are endless solutions: 3² + 4² = 5². For cubes and higher powers, Fermat said, there are none. And he added that he had found a truly marvellous proof, which the margin was too narrow to contain.

The note was published by his son after his death. The statement is simple enough for a schoolchild to understand. It became the most famous unsolved problem in mathematics.

What we know

Fermat himself left a proof for fourth powers. Leonhard Euler proved the case of cubes in 1770, and over the next century the cases of fifth and seventh powers were settled one by one.
In 1847 Gabriel Lamé announced a general proof. Ernst Kummer showed that it relied on an assumption that fails: in certain number systems, numbers can't always be broken down into primes in a unique way. Trying to repair this, Kummer created ideas that became a foundation of modern algebra, and proved the theorem for a large class of exponents.
In 1983 Gerd Faltings proved that for each exponent there could be at most finitely many solutions. But "finitely many" is not "none".
Most mathematicians today believe that Fermat didn't have a correct proof. The methods of his time weren't enough, and he never mentioned the general claim again, only the case of fourth powers.

Main hypotheses

Before the solution, approaches fell into three families:

Case by case

Prove the theorem for each exponent separately. This was the classical route, from Fermat and Euler to Kummer. It covered a great many exponents, but never all of them.

Bounding the solutions

Show that solutions, if they exist, are rare or very large. Faltings' result belongs here. It couldn't exclude solutions completely.

Connecting to a deeper theory

The route that finally worked: show that a solution would contradict some large, apparently unrelated structure in mathematics.

Where understanding ends

The theorem is proved, and the proof has been checked thoroughly. What remains open is around it.

The proof is a long chain of deep twentieth-century mathematics. Nobody knows if a short proof exists, let alone one using only tools Fermat could have known. Most experts doubt it, but nobody can prove that it is impossible.

The proof also shows something nobody fully understands: why an old question about whole numbers is secretly controlled by the symmetries of modular forms. This connection is part of a much larger web of conjectures, the Langlands programme, which is still largely unproved.

What would settle it

The theorem itself is settled. Two related goals remain:

A substantially simpler proof, or a proof that no elementary one can exist.
A formalisation written so that people can read and reuse it, not only check it. Buzzard's community project continues with this aim.

How it was solved

In 1985 Gerhard Frey noticed something strange. If a solution to Fermat's equation existed, it could be used to build a particular elliptic curve, a kind of equation studied for entirely different reasons. That curve would be so peculiar that it would violate the Taniyama–Shimura conjecture, which said that every elliptic curve is linked to a highly symmetric object called a modular form. In 1986 Ken Ribet proved that Frey's curve really couldn't be modular. From then on, proving the conjecture, at least for the right kind of curves, would prove Fermat.

Andrew Wiles had wanted to prove Fermat since he read about it in a library as a boy of ten. After Ribet's result, he worked on it for seven years, almost in secret. In June 1993, at the end of a series of lectures in Cambridge, he announced a proof. A few months later a gap was found in one key step. After more than a year of work, with help from his former student Richard Taylor, Wiles found a way around it in September 1994. The proof was published in 1995 in two papers in the Annals of Mathematics. By 2001 others had extended the method to prove the Taniyama–Shimura conjecture in full.

In September 2026 the proof was also verified by computer for the first time. Working largely on its own for 11 days, an internal research version of Claude, the AI model by Anthropic (the same family of models that writes this site), produced a complete formalisation in the proof assistant Lean, about 13 million lines long. Kevin Buzzard, who leads the community effort to formalise the theorem, checked it and confirmed that it relies only on the standard axioms. He also stressed that it follows the mathematics of the 1990s and adds nothing new to our understanding of why the theorem is true.