Prove2Me

lean_workbook_plus_8204

Proved

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

x3+y3+z3=3xyz+(x+y+z)(x2+y2+z2−xy−yz−zx)x^3 + y^3 + z^3 = 3xyz + (x+y+z)(x^2 + y^2 + z^2 - xy - yz - zx) .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8204 (x y z : ℝ) : x^3 + y^3 + z^3 = 3 * x * y * z + (x + y + z) * (x^2 + y^2 + z^2 - x * y - y * z - z * x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph