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.

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?

Yes, though not through my audit, which compared selected statements and did not reprove the papers or read every proof body. None of the differences I investigated was an error. But after the release, Ralph Furman of Anthropic had Claude review its work and posted five minor errors the agents found in supporting literature, none in the main FLT papers [7]. Two are in results the proof uses, and the formalization works around them; the other three are in papers it consulted but did not use:

  • Mennicke (1967), used for Ihara's lemma. It asserts that the Schur multiplier of \(\operatorname{SL}_2(\mathbb Z/m\mathbb Z)\) vanishes for every $ m $. Beyl showed in 1986 that it is $ \mathbb Z/2 $ exactly when $ 4 \mid m $, and repaired the argument. The Lean proof follows Beyl.
  • Lang, Elliptic Functions, Ch. 5, Thm. 3(ii), used. The modular polynomial is stated to be symmetric for all $ n $, but this fails for $ n = 1 $, where Lang's proof also breaks. The Lean version assumes $ n > 1 $.
  • Jordan–Livné (1985), Lemma 5.5(2), read but not used. The converse half, taken from Kurihara, fails when $ p \equiv 3 \pmod 4 $. It does no harm inside the paper.
  • Jordan–Livné (1986), Theorem 2.3, read but not used. The component-group formula is off by powers of 2 and 3; it gives $ 1/6 $ for a group of order 1. Papikian had published the same correction in 2016.
  • Edixhoven (1992), p. 583, read but not used. The least certain of the five: one step asserts a conclusion before the argument supports it. Reordering the paper's own ingredients fixes the proof.

A repair like Lang's shows up in Lean only as an extra hypothesis, $ n > 1 $, which a statement comparison can easily miss.

8. 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. R. Furman, message in the “Anthropic formalization” thread, Lean Zulip, #FLT, September 4, 2026. Zulip

Revised October 5, 2026. The first version of Section 7 said that no mathematical error in the literature had been established. That was true of my comparisons but not of the formalization, which found several minor errors; Section 7 and the abstract now describe them.