lean_workbook_plus_13444

Proved

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

Show that there are infinitely many pairs $(x, y)$ of rational numbers such that $x^3 +y^3 =9$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13444 : ∀ n : ℕ, ∃ x y : ℚ, x^3 + y^3 = 9   :=  by sorry

Source