lean_workbook_plus_33819

Disproved

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

Prove that the equation $x^3 + y^3 = 3xy$ has no integer solutions $(x, y)$ other than $(1, 1)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33819 (x y : ℤ) (h : x^3 + y^3 = 3 * x * y) : x = 1 ∧ y = 1   :=  by sorry

Source