lean_workbook_plus_30972

Disproved

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

Prove that the equation $y^2-x^3=1$ has only two integer solutions, which are $x=2,y=3$ or $x=2,y=-3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30972 : { (x,y) : ℤ × ℤ | y^2 - x^3 = 1}  =  {(2,3), (2,-3)}   :=  by sorry

Source