1. What Lean checked

  Anthropic's AI-generated Lean development proves Fermat's Last Theorem [1]. The final statement says that positive natural numbers cannot satisfy the Fermat equation for an exponent at least three:

theorem fermat_last_theorem
    (n : ℕ) (hn : 3 ≤ n)
    (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    a ^ n + b ^ n ≠ c ^ n

  The development proves FLT, but its intermediate results do not always match the cited papers. Some are specialized to Frey curves; others use different definitions or package constructions behind abstract interfaces. What do these changes tell us about how the classical proof was formalized?

  The repository's verification checks confirm that the code proves Mathlib's statement of FLT using only Lean's standard axioms [1]. The question here is what the intermediate results say and how they relate to the papers.

  I used a two-pass comparison. For each selected part of a paper, one AI agent compared its statements and constructions with the Lean source and reported the correspondences and differences. A second agent checked that report against both the paper and the code, challenging apparent mismatches and looking for overlooked declarations. The examples below include corrections made during that second pass.

  I audited revision aa2d8b3 of anthropics/fermats-last-theorem. All Lean links point to that fixed snapshot. Each comparison also identifies the numbered result and page in the paper, so the two statements can be checked directly.

2. What the comparisons establish

  The development follows the broad Frey–Serre–Ribet–Wiles strategy described by Darmon, Diamond, and Taylor [2]. After reducing to the relevant prime exponents, a hypothetical solution gives a Frey curve. Semistable modularity, proved using modularity lifting at 3 or 5, makes the curve modular. The curve's residual representation modulo the exponent $ p $ is then used for level lowering. Its irreducibility and modularity lead to a nonzero weight-two cusp form at level 2, where the cusp-form space is zero.

\[\text{counterexample} \longrightarrow E_{a,b,p} \longrightarrow \text{modular }E_{a,b,p} \longrightarrow \overline{\rho}_{E,p} \longrightarrow \text{level }2 \longrightarrow \bot.\]

  To see how the formal proof relates to this outline, we can compare a few steps directly: what the paper says, how Lean expresses it, and what that tells us about the argument. Sometimes Lean proves just the consequence needed for FLT. Elsewhere, understanding the connection requires looking beyond the displayed statement to definitions or constructions.

  Each card shows the paper statement alongside Lean code and an informal definition or theorem following the code's assumptions and conclusions. The surrounding discussion explains the comparison and any questions it leaves open. Code is copied from the pinned revision with line breaks adjusted.

3. Modularity after translation

  Darmon–Diamond–Taylor define a modular elliptic curve through equivalent geometric properties, including a modular parametrization and an isogeny to an abelian variety attached to a newform. Lean's WeierstrassCurve.IsModular instead asks for an integral model and a normalized weight-two form whose coefficients agree with the model's Frobenius traces at good primes away from its level.

  Proving modularity in this Lean formulation therefore supplies a form with the required coefficients. To recover a modular parametrization from that conclusion, one would need a theorem connecting the two descriptions. The audit did not locate that formal connection.

What “the curve is modular” means

Lean type 
def IsModularModelOfLevel
    (W : WeierstrassCurve ℤ) (N : ℕ) : Prop :=
  ∃ f : CuspForm (CongruenceSubgroup.Gamma0 N) 2,
    f.IsNormalizedEigenform ∧
    ∀ p : ℕ, p.Prime → W.IsGoodPrimeFor p → ¬ p ∣ N →
      ModularFormClass.qCoeff f p = (W.apOfModel p : ℂ)

def IsModularModel (W : WeierstrassCurve ℤ) : Prop :=
  ∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N

def IsModular (E : WeierstrassCurve ℚ) : Prop :=
  ∃ W : WeierstrassCurve ℤ,
    W.IsIntegralModelOf E ∧ W.IsModularModel
Informal meaning

Modular at a level. An integral Weierstrass model $W$ is modular at level $N$ if there exists a normalized weight-two cusp eigenform $f$ on $\Gamma_0(N)$ such that

$$a_p(f)=a_p(W)$$

for every prime $p$ at which the model $W$ has good reduction and which does not divide $N$. Here $a_p(f)$ is the coefficient of $q^p$ in $f$, and $a_p(W)$ is the Frobenius trace of the reduction of $W$.

Modular integral model. The model $W$ is modular if it is modular at some positive level $N$.

Modular rational curve. A Weierstrass curve $E$ over $\mathbb Q$ is modular if there exists an integral model $W$ of $E$ that is modular.

Paper statement

Let $E$ be any elliptic curve defined over $\mathbb Q$, and let $N$ denote its arithmetic conductor.

Proposition 1.53. The following are equivalent:

  1. The curve $E$ is isogenous over $\mathbb Q$ to $A_f$, for some newform $f$ on some congruence group $\Gamma$.
  2. The curve $E$ is isogenous over $\mathbb Q$ to $A_f$, for a newform $f$ on $\Gamma_0(N)$.
  3. There is a nonconstant morphism defined over $\mathbb Q$, from $X_0(N)$ to $E$.

We call an elliptic curve over $\mathbb Q$ satisfying the equivalent properties above a modular elliptic curve.

  Residual modularity has a similar translation. The paper identifies a residual Galois representation with one attached to an eigenform. Lean's FreyPackage.ModularRepOfLevel records coefficient congruences for a Frey curve, an eigenform, and a maximal ideal above the residual prime.

  Here Lean works specifically with the packaged Frey curve. What the definition supplies is agreement of coefficients modulo a maximal ideal; identifying this with the paper's representation isomorphism requires a further argument that the audit did not establish in Lean.

What “the residual representation is modular at level N” means

Lean type 
def ModularRepOfLevel (P : FreyPackage) (N : ℕ) : Prop :=
  ∃ (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2)
      (W : WeierstrassCurve ℤ)
      (𝔪 : Ideal (integralClosure ℤ ℂ)),
    f.IsNormalizedEigenform ∧
    W.IsIntegralModelOf P.freyCurve ∧
    𝔪.IsMaximal ∧
    (P.p : integralClosure ℤ ℂ) ∈ 𝔪 ∧
    ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ →
      ¬ ℓ ∣ N → ℓ ≠ P.p →
      ∃ a : integralClosure ℤ ℂ,
        (a : ℂ) = ModularFormClass.qCoeff f ℓ ∧
        a - ((W.apOfModel ℓ : ℤ) : integralClosure ℤ ℂ) ∈ 𝔪
Informal meaning

Fix a Frey package $P$ and a natural number $N$, and write $p=P.p$. Let $\mathcal A$ be the ring of algebraic integers in $\mathbb C$.

By definition, $P$ satisfies ModularRepOfLevel N if there exist a normalized weight-two cusp eigenform $f$ on $\Gamma_0(N)$, an integral model $W$ of $P$'s Frey curve, and a maximal ideal $\mathfrak m$ of $\mathcal A$ containing $p$, with the following property:

For every prime $\ell$ at which $W$ has good reduction, with $\ell\nmid N$ and $\ell\ne p$, there is an element $a\in\mathcal A$ whose image in $\mathbb C$ equals $a_\ell(f)$ and for which

$$a-a_\ell(W)\in\mathfrak m.$$

Equivalently, at these primes the coefficient $a_\ell(f)$ is an algebraic integer congruent to the Frobenius trace $a_\ell(W)$ modulo $\mathfrak m$.

Paper statement

Definition 3.12. We say that a representation

$$\overline\rho:G_{\mathbb Q}\longrightarrow\operatorname{GL}_2(k)$$

is modular (of level $N$) if, for some newform $f$ of weight 2 and level $N$, $\overline\rho$ is equivalent over $k_f$ to $\overline\rho_f$.

4. Specializing Mazur and Ribet

  Mazur's theorem restricts the possible prime degrees of rational cyclic isogenies for elliptic curves over $\mathbb Q$ [3]. For FLT, the relevant consequence is irreducibility of the residual representation of a normalized Frey curve. The declaration FreyPackage.Mazur_Frey states this consequence directly.

  This gives the irreducibility result needed for the Frey curve. It tells us nothing about the possible isogeny degrees of an arbitrary elliptic curve, so the declaration alone cannot be read as a formalization of Mazur's full classification.

Mazur: classification becomes irreducibility

Lean type 
theorem FreyPackage.Mazur_Frey (P : FreyPackage) :
  GaloisRepIsIrreducible
    (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p
Informal meaning

Let $P$ be a Frey package, let $E=P.\mathrm{freyCurve}$, and let $p=P.p$. Then the action of $G_{\mathbb Q}$ on $E[p](\overline{\mathbb Q})$ is irreducible over $\mathbb F_p$: its only Galois-invariant linear subspaces are zero and the whole space.

The assumption that $P$ is a FreyPackage includes the hypotheses stored in that structure.

Paper statement

Theorem 1. Let $N$ be a prime number such that some elliptic curve over $\mathbb Q$ admits a $\mathbb Q$-rational $N$-isogeny. Then

$$N=2,3,5,7,13,$$

or

$$N=11,17,19,37,43,67,163.$$

  Ribet's theorem removes a prime from the level of an irreducible modular residual representation [4]. The displayed Lean theorem fixes a FreyPackage, assumes conductor, irreducibility, modularity, and unramifiedness conditions, and produces a divisor level avoiding the selected prime.

  Ribet starts at level $Mp$, with $p$ not dividing $M$, and concludes modularity at $M$. Lean allows a divisor of the input level from which the selected prime has disappeared. Thus the formal conclusion gives a level avoiding that prime, without specifying the exact quotient appearing in Ribet's statement.

Ribet: lowering to a suitable divisor

Lean type 
theorem FreyPackage.level_lowering_odd_prime_of_conductorLevel
    (P : FreyPackage) {N q : ℕ}
    (hcond : P.IsConductorLevel N)
    (hq : q.Prime) (hq2 : q ≠ 2) (hqp : q ≠ P.p)
    (hqN : q ∣ N)
    (hirr : GaloisRepIsIrreducible
      (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p)
    (hmod : P.ModularRepOfLevel N)
    (hunr : P.GaloisRepUnramifiedAt q) :
    ∃ M : ℕ,
      M ∣ N ∧ ¬ q ∣ M ∧ P.ModularRepOfLevel M
Informal meaning

Let $P$ be a Frey package, write $p=P.p$, and let $N,q\in\mathbb N$. Assume:

  • $N$ satisfies the package's conductor-level predicate P.IsConductorLevel N;
  • $q$ is prime, $q\ne 2$, $q\ne p$, and $q\mid N$;
  • the mod-$p$ Galois representation of the Frey curve is irreducible;
  • $P$ satisfies ModularRepOfLevel N, the coefficient-congruence definition above;
  • the representation is unramified at $q$, as expressed by P.GaloisRepUnramifiedAt q.

Then there exists $M\in\mathbb N$ such that $M\mid N$, $q\nmid M$, and $P$ satisfies ModularRepOfLevel M.

Paper statement

Theorem 8.2 (Main Theorem). Let

$$\rho:\operatorname{Gal}(\overline{\mathbb Q}/\mathbb Q)\longrightarrow \operatorname{GL}(2,\mathbb F)$$

be an irreducible mod-$\ell$ modular representation of level $Mp$, where $p$ is a prime not dividing $M$. Assume that $\rho$ is finite at $p$. Then $\rho$ is modular of level $M$, provided that at least one of the following conditions holds:

  1. the prime $\ell$ is not a divisor of $M$;
  2. $p\not\equiv 1\pmod{\ell}$.

  The formal development ultimately produces a nonzero cusp form at level 2 and contradicts the vanishing of that space. This explains why the specialized level-lowering result is useful without identifying it with Ribet's full theorem.

5. Construction versus interface

  Taylor–Wiles patching separates an algebraic argument from the arithmetic construction of its inputs [5]. The paper constructs deformation rings, Hecke rings, and compatible data at auxiliary levels. Its appendix also gives an abstract ring-theoretic criterion, Proposition 3, used to prove the concrete $R=\mathbb T$ result below.

  Lean's PatchingDatum likewise packages objects at varying levels, maps, bounds, and compatibility conditions. Given this structure, the displayed theorem proves an isomorphism, freeness, and a presentation with as many relations as variables. Comparing it with the paper's concrete theorem raises a question about how those abstract inputs are supplied.

  The remaining question is where the formal proof obtains these data. If the final proof uses this theorem, its patching-data hypothesis must be discharged somewhere along that route. The audit did not establish that dependence or identify a concrete datum built from the paper's deformation and Hecke rings, so this comparison stops at what the abstract theorem proves.

Taylor–Wiles: abstract data and a concrete theorem

Lean type 
theorem Algebra.PatchingDatum.bijective_and_free_of_surjective
    {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪]
    [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
    [Finite (IsLocalRing.ResidueField 𝒪)]
    {ℓ r : ℕ} (hℓ : (ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪)
    {R : Type} [CommRing R] [Algebra 𝒪 R]
    {M : Type} [AddCommGroup M] [Module R M] [Nontrivial M]
    (P : Algebra.PatchingDatum 𝒪 ℓ r R M)
    {T : Type} [CommRing T] [Algebra 𝒪 T] [Module T M]
    (RtoT : R →ₐ[𝒪] T) (hsurj : Function.Surjective RtoT)
    (hcompat : ∀ x m, RtoT x • m = x • m) :
    Function.Bijective RtoT ∧
    Module.Free R M ∧ Module.Free T M ∧
    Module.annihilator R M = ⊥ ∧
    ∃ f : Fin r → MvPowerSeries (Fin r) 𝒪,
      Nonempty
        ((MvPowerSeries (Fin r) 𝒪 ⧸ Ideal.span (Set.range f))
          ≃ₐ[𝒪] T)
Informal meaning

Let $\mathcal O$ be a complete discrete valuation ring with finite residue field. Let $\ell,r\in\mathbb N$, with the image of $\ell$ in the maximal ideal of $\mathcal O$. Let $R$ and $T$ be commutative $\mathcal O$-algebras, and let $M$ be a nonzero module over both rings.

Assume that patching data $P$ of type Algebra.PatchingDatum 𝒪 ℓ r R M are given, together with a surjective $\mathcal O$-algebra map $\varphi:R\to T$ satisfying

$$\varphi(x)m=xm\qquad(x\in R,\ m\in M),$$

where the left side uses the $T$-action and the right side uses the $R$-action. Then:

  • $\varphi$ is an isomorphism;
  • $M$ is free over $R$ and over $T$;
  • the only element of $R$ annihilating every element of $M$ is zero;
  • there exist $r$ formal power series $f_1,\ldots,f_r$ in $r$ variables over $\mathcal O$ and an isomorphism of $\mathcal O$-algebras

$$\mathcal O[[X_1,\ldots,X_r]]/(f_1,\ldots,f_r)\simeq T.$$

Paper statement

Here $R$ is the universal deformation ring for the appendix's deformation problem with no auxiliary primes, and $\mathbb T$ is the corresponding Hecke ring.

Theorem 3. The natural map is an isomorphism

$$R\mathbin{\overset{\sim}{\longrightarrow}}\mathbb T,$$

and these rings are complete intersections.

Sources Lean theorem · Taylor–Wiles, Appendix, Theorem 3, p. 19 of the linked PDF [5]

6. A closer match: the 3–5 switch

  In Wiles's semistable modularity argument, the 3–5 switch produces an auxiliary elliptic curve with the same mod-5 representation and an irreducible mod-3 representation [6]. The Lean declaration named threeFiveSwitchCurve records congruences of good-prime traces. Reading only that statement would miss the stronger nearby theorem threeFiveAuxiliaryCurveExists, which supplies a Galois-equivariant isomorphism on 5-torsion.

  In this case the two desired properties are visible in Lean's statement: irreducibility at 3 and an isomorphism on 5-torsion commuting with the Galois action. Passing to integral Weierstrass models changes the presentation, but the auxiliary curve has the properties stated in Darmon–Diamond–Taylor's lemma. Whether it is constructed by the same argument is a separate question.

The 3–5 switch: follow the stronger declaration

Lean type 
theorem WeierstrassCurve.threeFiveAuxiliaryCurveExists
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0)
    (hW : W.IsSemistableModel)
    (h5 : W.ModRepIsIrreducible 5) :
    ∃ W' : WeierstrassCurve ℤ,
      W'.Δ ≠ 0 ∧ W'.IsSemistableModel ∧
      W'.ModRepIsIrreducible 3 ∧
      ∃ φ : Submodule.torsionBy ℤ
          ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point
          (5 : ℕ)
        ≃ₗ[ZMod 5]
          Submodule.torsionBy ℤ
          ((W'.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point
          (5 : ℕ),
        ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
          (x : Submodule.torsionBy ℤ
            ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point
            (5 : ℕ)),
          φ (σ • x) = σ • φ x
Informal meaning

Let $W$ be an integral Weierstrass model with nonzero discriminant. Assume that $W$ is semistable and that its mod-5 Galois representation is irreducible.

Then there exists an integral Weierstrass model $W'$ with nonzero discriminant such that $W'$ is semistable, its mod-3 Galois representation is irreducible, and there is an $\mathbb F_5$-linear isomorphism

$$\varphi:E[5](\overline{\mathbb Q})\longrightarrow E'[5](\overline{\mathbb Q}),$$

where $E$ and $E'$ are the rational curves defined by $W$ and $W'$. This isomorphism satisfies

$$\varphi(\sigma x)=\sigma\varphi(x)$$

for every $\sigma\in G_{\mathbb Q}$ and every 5-torsion point $x$ of $E$.

Paper statement

Lemma 3.49. There is an auxiliary (semistable) elliptic curve $A/\mathbb Q$ which satisfies:

  1. $A[5]\simeq E[5]$ as $G_{\mathbb Q}$-modules;
  2. $A[3]$ is an irreducible $G_{\mathbb Q}$-module.
Sources Lean theorem · Darmon–Diamond–Taylor, Lemma 3.49, p. 103 [2]

7. Did formalization find an error?

  None of the investigated differences established a mathematical error in the literature or Lean. The audit compared selected statements, definitions, and construction boundaries. It did not independently reprove the papers, inspect every formal theorem body, or reconstruct the final kernel proof term. Unresolved correspondences remain unresolved.

  The second reading corrected some initial findings. The 3–5 switch above was first judged from the weaker declaration, before the torsion-isomorphism theorem was located. An initial claim that Shimura-curve geometry was absent also had to be withdrawn when substantial Cerednik–Drinfeld infrastructure was found. Finding a different interface had been mistaken for finding missing mathematics.

  One remaining question is concrete enough to check directly. Rubin and Silverberg give coefficient formulas for families of elliptic curves with constant mod-$p$ representations [7]. Lean contains families rsFamilyA and rsFamilyB and proves the existence of bounded-degree polynomial representatives. The audit did not identify the printed formulas with these families term by term after normalization. That calculation would settle a correspondence the present comparison leaves open.

  The regular-prime case provides a useful control. Best, Birkbeck, Brasca, Rodriguez Boidi, van de Velde, and Yang formalized Kummer's argument in Lean [8]; the audited development ports that work. The audit found direct correspondence for the final theorem and the main Hilbert 90, 92, and 94 steps. Differences were chiefly the unfolding of the regularity predicate, library names, and normalization. Here the evidence supports a close correspondence beyond the final statement.

8. Conclusion

  The Lean development proves FLT through a recognizable classical strategy. The comparisons show how much the intermediate formulation can vary: Mazur and Ribet appear in specialized forms, modularity is expressed through coefficients, and an abstract patching theorem leaves its arithmetic application to be traced. The 3–5 switch and regular-prime case show closer matches. This still leaves some intermediate results to be checked against their counterparts in the literature, even though Lean has checked their formal proofs.

9. References

  1. Anthropic, Fermat's Last Theorem in Lean 4 (2026). GitHub
  2. H. Darmon, F. Diamond, and R. Taylor, Fermat's Last Theorem, Current Developments in Mathematics 1995, 1–154. Link
  3. B. Mazur, Rational isogenies of prime degree, Invent. Math. 44 (1978), 129–162. Link
  4. K. A. Ribet, On modular representations of $\operatorname{Gal}(\overline{\mathbb Q}/\mathbb Q)$ arising from modular forms, Invent. Math. 100 (1990), 431–476. Link
  5. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Ann. of Math. 141 (1995), 553–572. Link
  6. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Ann. of Math. 141 (1995), 443–551. Link
  7. K. Rubin and A. Silverberg, Families of elliptic curves with constant mod $p$ representations, in Elliptic Curves, Modular Forms, & Fermat's Last Theorem (1995), 148–161. Link
  8. A. J. Best, C. Birkbeck, R. Brasca, E. Rodriguez Boidi, R. van de Velde, and A. Yang, A complete formalization of Fermat's Last Theorem for regular primes in Lean, Annals of Formalized Mathematics 1 (2025), 103–132. arXiv