lean_workbook_plus_55873

Proved

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

Show that the equation $3y^{2}= x^{4}+x$ has no solutions in positive integers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55873 (x y : ℤ) (h₁ : 0 < x ∧ 0 < y) (h₂ : 3*y^2 = x^4 + x) : False   :=  by sorry

Source