lean_workbook_plus_11282

Proved

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

Show that the equation $x^2+8y=3+2z^2$ has no solutions of positive integers $x,y$ and $z$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11282 (x y z : ℕ) (h₁ : 0 < x ∧ 0 < y ∧ 0 < z) (h₂ : x^2 + 8*y = 3 + 2*z^2) : False   :=  by sorry

Source