lean_workbook_plus_80487

Proved

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

First note that $2z^{2} = 3xy$ . So, we have $x^3 + y^3 + z^3 = x^3 + y^3 + (-z)^3 - 3xy(-z)$ which we can factor as $(x + y - z)(x^2 + zx - xy + zy + z^2 + y^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80487  (x y z : ℂ)
  (h₀ : 2 * z^2 = 3 * (x * y))
  (h₁ : x^3 + y^3 + z^3 = x^3 + y^3 + (-z)^3 - 3 * (x * y) * (-z)) :
  x^3 + y^3 + z^3 = (x + y - z) * (x^2 + z * x - x * y + z * y + z^2 + y^2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph