by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
If a+b+c=x+y+z=0 prove that \n\n 4(ax+by+cz)3−3(ax+by+cz)(a2+b2+c2)(x2+y2+z2)−2(a−b)(b−c)(c−a)(x−y)(y−z)(z−x)=54abcxyz
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_45164 : ∀ a b c x y z : ℝ, a + b + c = 0 ∧ x + y + z = 0 → 4 * (a * x + b * y + c * z) ^ 3 - 3 * (a * x + b * y + c * z) * (a ^ 2 + b ^ 2 + c ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2) - 2 * (a - b) * (b - c) * (c - a) * (x - y) * (y - z) * (z - x) = 54 * a * b * c * x * y * z := by sorry