Worked solution: Wiles's modularity proof via the Taylor–Wiles method (1994)

Combining Theorem 0.4 of Wiles (1995, p. 448: every semistable elliptic curve over $\mathbb{Q}$ is modular) with Ribet's theorem (Step 6) immediately yields Theorem 0.5 of Wiles (1995, p. 448): if $u^p + v^p + w^p = 0$ with $u, v, w \in \mathbb{Q}$ and prime $p \ge 3$, then $uvw = 0$. Equivalently, there are no nonzero integers $x, y, z$ and integer $n > 2$ such that $x^n + y^n = z^n$ (Qiu et al. 2025, Section 3.1.3).

Let us trace the complete logical chain one last time: (1) any counterexample for $n > 2$ reduces to $n = 4$ (ruled out by Fermat), $p = 3$ (ruled out by Euler), or a pairwise coprime counterexample $a^p + b^p = c^p$ for a prime $p \ge 5$; (2) a coprime counterexample for $p \ge 5$ produces the semistable Frey curve $E_{a,b,c}: y^2 = x(x - a^p)(x + b^p)$ of conductor $N = \operatorname{rad}(abc)$; (3) by Langlands–Tunnell at $p = 3$, the $3$–$5$ switch, and the $R_{\Sigma} \cong \mathbb{T}_{\Sigma}$ theorem proved via Taylor–Wiles patching, every semistable elliptic curve over $\mathbb{Q}$ is modular, so $E_{a,b,c}$ is modular; (4) by Ribet's level-lowering theorem, modularity of $E_{a,b,c}$ forces a nonzero weight-$2$ cusp form in $S_2(\Gamma_0(2)) = \{0\}$, a contradiction.

Following the publication of Wiles's and Taylor–Wiles's papers in the May 1995 issue of the Annals of Mathematics, the methods they introduced transformed number theory: Breuil, Conrad, Diamond, and Taylor proved the full Modularity Theorem for all elliptic curves over $\mathbb{Q}$ in 1999, Khare and Wintenberger proved Serre's full modularity conjecture in 2004–2008 (giving a second modern route to FLT), and an ongoing project led by Kevin Buzzard (begun in 2024) is formalizing the complete proof in the Lean theorem prover (Qiu et al. 2025, Section 2.3).