lean_workbook_plus_74741

Proved

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

The equation $a^{3} +b^{3} =c^{3}$ does have the integer solution $(a, b, c) = (0,0,0)$ and $(a,b,c) = (k, -k, 0)$ for some $k \in \mathbb{Z}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74741 : ∃ a b c : ℤ, a^3 + b^3 = c^3 ∧ (a = 0 ∧ b = 0 ∧ c = 0) ∨ (∃ k : ℤ, a = k ∧ b = -k ∧ c = 0)   :=  by sorry

Source