Prove2Me

Rational points of Y2=X(X2+30X+289)Y^2=X(X^2+30X+289), a model of X0(17)X_0(17)

Proved
MazurHuang.x0_seventeen_two_isogeny_model_points

by xuanji · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-curvesmazur-full-torsionnumber-theory

Every rational affine point (X,Y)(X,Y) on the elliptic curve

Y2=X(X2+30X+289)Y^2=X(X^2+30X+289)

has X=0X=0 or X=17X=17. Equivalently the rational points are ∞\infty, (0,0)(0,0) and (17,±136)(17,\pm136), a cyclic group of order 44 (rank zero).

This curve is the two-isogeny-translated model of X0(17)X_0(17) (Cremona 17a1, y2+xy+y=x3−x2−x−14y^2+xy+y=x^3-x^2-x-14). It is the arithmetic input to the exclusion of rational points of order 1717 in Xiang Huang's Lean development.

Preamble
import Mathlib

open scoped WeierstrassCurve.Affine
Formal statement
theorem MazurHuang.x0_seventeen_two_isogeny_model_points (X Y : ℚ)
    (h : Y ^ 2 = X ^ 3 + 30 * X ^ 2 + 289 * X) : X = 0 ∨ X = 17 := by sorry
Source
Xiang Huang, FLT fork, commit 51bbb4f191ad0d3753b87123635c100a638ae580 (Apache-2.0), https://github.com/xiangyazi24/FLT/blob/51bbb4f191ad0d3753b87123635c100a638ae580/FLT/Assumptions/MazurProof/X017RationalPoints.lean (theorem eq_zero_or_K_or_T_or_neg_T on the standard model Y²=X(X²+a17·X+b17), a17=30, b17=289 in X017Model.lean).

View graph