lean_workbook_plus_15684

Proved

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

Prove that the equation $x^3+3y^3+9z^3-9xyz=1$ has infinitely many integer solutions $(x,y,z)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15684 : ∃ c : ℤ, ∀ d : ℤ, ∃ x y z : ℤ, x^3 + 3 * y^3 + 9 * z^3 - 9 * x * y * z = 1 ∧ x > c ∧ y > c ∧ z > c   :=  by sorry

Source