Fermat’s Last Theorem, checked line by line

If $n = mk$, a solution with exponent $n$ gives one with exponent $k$, because $a^n + b^n = c^n$ is the same equation as

Every $n \ge 3$ is divisible by $4$ or by an odd prime, so it suffices to rule out $n = 4$ and $n = p$ for odd primes $p$. Fermat himself settled $n = 4$ by infinite descent: from a solution of $x^4 + y^4 = z^2$ in positive integers he built a smaller one, which is impossible because positive integers cannot decrease forever. Euler handled $p = 3$.

Suppose $a^p + b^p = c^p$ for a prime $p \ge 5$, with $a$, $b$, $c$ positive and without common factors. Frey and Hellegouarch attached to it the elliptic curve

Its discriminant, computed from the differences of the three roots $0$, $a^p$ and $-b^p$, is

a perfect $p$-th power up to the factor $16$. That makes the curve strange: it has bad reduction only at primes dividing $abc$, and in a way that the arithmetic of its points modulo $p$ barely notices.

Serre predicted, and Ribet proved in 1986, that if $E$ were modular, its points modulo $p$ would be governed by a modular form of weight $2$ and level $2$. There is no such form: the space of these cusp forms is zero, $\dim S_2(\Gamma_0(2)) = 0$.

Wiles, with Taylor, proved that every semistable elliptic curve over $\mathbb{Q}$ is modular, and the Frey curve is semistable. So $E$ is modular and cannot be modular at the same time. The only way out is that the solution $a$, $b$, $c$ never existed.

The final Lean statement is elementary, but every link above rests on a large theory: Galois representations, modular forms and Hecke algebras, and the Taylor–Wiles method for proving modularity. A formal proof must build all of it from the definitions, and a small kernel then checks each inference. That is why formalizing a proof whose conclusion fits on one line takes millions of lines.