lean_workbook_plus_59919

Proved

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

Find all pairs of positive integers (x,y) such that: $x^2-6y^2=-3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59919 (x y : ℤ) (h₁ : 0 < x ∧ 0 < y) (h₂ : x^2 - 6*y^2 = -3) : x = 3 ∧ y = 1   :=  by sorry

Source