Input A Weierstrass equation
Coefficients of y2 + a1xy + a3y = x3 + a2x2 + a4x + a6, as integers (the curve must be smooth, i.e. Δ ≠ 0).
What is assumed. We take the full modularity theorem as a black box (every semistable elliptic curve over ℚ is modular) and therefore do not verify semistability here. The app computes exactly the data the theorem consumes, and shows the eigenform recursion it produces. Nothing is proved by the app; the proof lives in the Lean files linked at the bottom.
Trace From each computed step to the Lean proof
Every quantity below is a Lean object. Line numbers are pinned to anthropics/fermats-last-theorem@aa2d8b3.
| Computed here | Mathematics | Lean (pinned sha) |
|---|---|---|
| integral model | E : y²+a₁xy+a₃y = x³+a₂x²+a₄x+a₆, aᵢ ∈ ℤ | WeierstrassCurve ℤ |
| minimal model | integral model with vp(Δ) minimal at every p | IsIntegralModelOf, lines 88–90 (an existential over VariableChange ℚ) |
| discriminant Δ | Δ = −b₂²b₈ − 8b₄³ − 27b₆² + 9b₂b₄b₆ | WeierstrassCurve.Δ |
| conductor level | the squarefree level supported on the bad primes | conductorLevel W := radical W.Δ.natAbs; for the Frey package IsConductorLevel, lines 8–14 |
| reduction mod p | reduce the coefficients modulo p | reductionMod, lines 76–77 |
| #E(𝔽p) | 1 + #{(x,y) ∈ 𝔽p² : the equation holds} | Point.instFinite / WeierstrassCurve.card, lines 61–70 |
| trace ap | ap = p + 1 − #E(𝔽p) | traceOfFrobenius, apOfModel, lines 72–80 |
| good prime | p ∤ Δ | IsGoodPrimeFor, lines 82–83 |
| eigenform recursion | a₁ = 1; amn = aman (coprime); apr+2 = apapr+1 − p·apr (p ∤ N); apr+2 = apapr+1 (p | N) | IsNormalizedEigenform, lines 28–40 |
| modularity | ap(f) = ap(E) at all good p ∤ N | IsModularModelOfLevel / IsModularModel / IsModular, lines 93–102 |
| semistability (assumed, not checked) | p | Δ ⇒ p ∤ c₄ | IsSemistableModel, lines 85–87 |
| the theorem | semistable E/ℚ ⇒ E is modular (Wiles) | WeierstrassCurve.modularity_of_semistableModel; Frey case FreyPackage.frey_isModular |
| level lowering | Frey curve modular + E[p] irreducible ⇒ a nonzero form at level 2 | FreyPackage.level_lowering_to_two |
| the endgame | S₂(Γ₀(2)) = 0 — no such form exists | ModularForm.S2_Gamma0_2_eq_zero |
Why What the computation has to do with Fermat
A counterexample ap + bp = cp (p ≥ 5 prime, abc ≠ 0, primitive) produces the Frey curve EP : y² + xy = x³ + ((bp−1−ap)/4)x² − (apbp/16)x. Its discriminant is Δ = (abc)2p/2⁸, so its bad primes are exactly the primes of abc, and it is semistable. Wiles's theorem makes it modular; Ribet's level-lowering theorem strips the bad primes one at a time, leaving a nonzero weight-2 cusp form of level 2; and S₂(Γ₀(2)) = 0. Contradiction.
The app is a window on the first and last of those links: it computes the level N that Wiles's theorem feeds on, and the coefficient sequence that Ribet's congruence then has to force to zero at level 2. (A genuine Frey curve requires a genuine counterexample, which does not exist; the “Frey-type” preset uses arbitrary a, b, p of the right shape to show the arithmetic.)