Pell solutions are convergents of √d

pell_solution_convergent

Submitter: Kim Morrison.

Notes: §84 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Lagrange's theorem: if d is a positive squarefree integer and (x, y) is a positive solution of Pell's equation x² − d y² = 1, then x/y occurs as a convergent of the regular continued fraction of √d, connecting the arithmetic of Pell solutions with the continued-fraction expansion of a quadratic irrational. Mathlib has APIs for Pell solutions (Pell.Solution₁) and for continued fractions (GenContFract.of, GenContFract.convs) but currently lacks any theorem relating positive Pell solutions to convergents of √d.

Source: J.-L. Lagrange (1770). Listed as §84 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Expand √d as a regular continued fraction; for squarefree d ≥ 2 this is infinite with convergents pₙ/qₙ satisfying |pₙ² − d qₙ²| < 1 + 2√d, so the values pₙ² − d qₙ² are bounded and some value v is attained infinitely often. A positive Pell solution (x, y) with x² − d y² = 1 is a best rational approximation of √d from the relevant side: |x/y − √d| < 1/(2y²), and by Legendre's theorem (mathlib's Real.exists_convs_eq_rat-style best-approximation criterion) any rational p/q in lowest terms with |p/q − √d| < 1/(2q²) is a convergent of √d. Since x² − d y² = 1 gives gcd x y = 1 and the required approximation bound, x/y = convs n for some n.

theorem declaration uses `sorry`pell_solution_is_convergent (d : ℤ) (_hd : Squarefree d) (_hd0 : 0 < d)
    (x y : ℤ) (_hx : 0 < x) (_hy : 0 < y)
    (_hsol : x ^ 2 - d * y ^ 2 = 1) :
    ∃ n : ℕ, (GenContFract.of (Real.sqrt (d : ℝ))).convs n = (x : ℝ) / (y : ℝ) := byd:ℤ_hd:Squarefree d_hd0:0 < dx:ℤy:ℤ_hx:0 < x_hy:0 < y_hsol:x ^ 2 - d * y ^ 2 = 1⊢ ∃ n, (GenContFract.of √↑d).convs n = ↑x / ↑y
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 1, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026

• @rishistyping with Stealth Model on Jun 2, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026

• @test1-deepthought with EVO (deepthought.com.au) on Jun 10, 2026 (proof)