lean_workbook_plus_38473

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

The equation $x^{2}-dy^{2}=1$ , where $d \in \mathbb N$ , $d$ not a perfect square, is named Pell's equation and has an infinity of solutions $(x,y) \in \mathbb Z^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38473 (d : ℕ) (h₁ : ¬ ∃ k : ℕ, k^2 = d) (h₂ : 0 < d) : ∃ n : ℕ, ∃ x y : ℤ, x^2 - d*y^2 = 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph