Prove2Me

lean_workbook_plus_69589

Proved

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

Put a=x3−1,b=(x+1)3+1a=x^3-1, b=(x+1)^3+1 to get a3+b3=(a+b)3  ⟺  ab(a+b)=0a^3+b^3=(a+b)^3\iff ab(a+b)=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69589 (x a b : ℤ) (ha : a = x^3 - 1) (hb : b = (x + 1)^3 + 1) :
  a^3 + b^3 = (a + b)^3 ↔ a * b * (a + b) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph