lean_workbook_plus_10941

Proved

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

In the equation $(x+y+z)^3 = x^3+y^3+z^3+6xyz+3(x^2y+x^2z+...)$ , if $xyz=-2$ , what are the possible values of $x+y+z$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10941 (x y z : ℝ) (h : x*y*z = -2) : (x + y + z)^3 = x^3 + y^3 + z^3 + 6*x*y*z + 3*(x^2*y + x^2*z + y^2*x + y^2*z + z^2*x + z^2*y)   :=  by sorry

Source

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

View graph