Motivation

Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' Arithmetica, that no $n$-th power with $n > 2$ splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.

Timeline. Fermat himself proved the case $n = 4$ by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated $n = 3$ in his Vollständige Anleitung zur Algebra (1770), by a descent in $\mathbb{Z}[\sqrt{-3}]$ that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled $n = 5$ between 1825 and 1830, Dirichlet added $n = 14$ in 1832, and Lamé published $n = 7$ in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in $\mathbb{Z}[\zeta_p]$, he proved the theorem for every regular prime exponent — those $p$ not dividing the class number of $\mathbb{Q}(\zeta_p)$, a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.

The route that closed the problem came from a different direction. The modularity conjecture of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over $\mathbb{Q}$ arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution $a^p + b^p = c^p$ the curve $y^2 = x(x - a^p)(x + b^p)$, whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over $\mathbb{Q}$ implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 Annals of Mathematics papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.

Setting

Fix a natural number $n$ and natural numbers $a, b, c$. A Fermat triple of exponent $n$ is a triple $(a,b,c)$ of strictly positive naturals with

$$a^n + b^n = c^n.$$

For $n = 1$ such triples are everywhere, and for $n = 2$ they are the Pythagorean triples, parametrized by $(k(u^2-v^2),\, 2kuv,\, k(u^2+v^2))$. The assertion at issue is that from $n = 3$ upward there are none at all: the hypothesis $3 \le n$ and the positivity hypotheses $0 < a$, $0 < b$, $0 < c$ are exactly what is needed, since $n \le 2$ and the degenerate triples with a zero entry both produce solutions.

Two standard reductions organize any attack. First, if $(a,b,c)$ is a triple of exponent $n$ and $m \mid n$, then $(a^{n/m}, b^{n/m}, c^{n/m})$ is a triple of exponent $m$; since every $n \ge 3$ is divisible by $4$ or by an odd prime $p \ge 3$, the general statement follows from the cases $n = 4$ and $n = p$ an odd prime. Second, for a prime exponent $p$ one may assume $\gcd(a,b,c) = 1$, and the classical literature then splits on whether $p \nmid abc$ (case I) or $p \mid abc$ (case II).

Formalization targets

Goal

$$\forall\, n \ge 3,\ \forall\, a, b, c \in \mathbb{N}_{>0},\qquad a^n + b^n \ne c^n.$$

This is the mission's single goal, referenced as the published platform theorem fermat_last_theorem. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.

Significance

The result itself. As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over $\mathbb{Q}$, made modularity lifting ("$R = T$") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.

Formalizing it. The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases $n = 3$ and $n = 4$, and the flt-regular project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.

Difficulty

The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle $n = 3, 4, 5, 7$ depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in $\mathbb{Z}[\zeta_n]$ or a substitute, and unique factorization fails there for all but finitely many $n$. Kummer's ideal-theoretic repair recovers the argument exactly when $p$ is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over $\mathbb{Q}$, their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.

Formalization scope

The target is stated over $\mathbb{N}$, so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over $\mathbb{Z}$ and over $\mathbb{Q}$ follow by clearing denominators and moving terms, and a solver who prefers to work over $\mathbb{Z}$ must supply that bridge. Exponentiation is Monoid.npow on $\mathbb{N}$, and $0^0 = 1$ plays no role because $3 \le n$. The hypotheses $0 < a$, $0 < b$, $0 < c$ are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.

A complete development will want: the reduction from general $n$ to $n = 4$ and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over $\mathbb{Q}$, conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.

Selected references

• Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• Richard Taylor and Andrew Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• Kenneth A. Ribet, On modular representations of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476. https://doi.org/10.1007/BF01231195
• Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor, On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
• Ernst Eduard Kummer, Beweis des Fermat'schen Satzes der Unmöglichkeit von $x^\lambda + y^\lambda = z^\lambda$ für eine unendliche Anzahl Primzahlen $\lambda$, Monatsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin (1847), 132–139.
• Gerhard Frey, Links between stable elliptic curves and certain Diophantine equations, Annales Universitatis Saraviensis 1 (1986), 1–40.
• Riccardo Brasca et al., Fermat's Last Theorem for regular primes (flt-regular), Lean 4 formalization. https://github.com/leanprover-community/flt-regular
• Kevin Buzzard et al., The Fermat's Last Theorem project, Lean 4 formalization in progress. https://imperialcollegelondon.github.io/FLT/