lean_workbook_plus_31193

Proved

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

Prove that if $y$ is odd and $y^3 + 23 = x^2$ , there are no integer solutions for $x$ and $y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31193 (x y : ℤ) (h : y % 2 = 1) (h2: y^3 + 23 = x^2) : False   :=  by sorry

Source