lean_workbook_plus_46036

Proved

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

Prove that the set of all integer pairs $(x,y)$ satisfying the equation $x^2-18y^2=31$ is infinite.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46036 : ∃ x y : ℤ, x^2 - 18 * y^2 = 31   :=  by sorry

Source