Prove2Me

lean_workbook_plus_62612

Proved

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

Prove that x3y+y3z+z3x=−9x^3y+y^3z+z^3x=-9 given x+y+z=0x+y+z=0 and x2+y2+z2=6x^2+y^2+z^2=6.

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

View graph