lean_workbook_plus_69684

Proved

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

If $x + y + z = 0$ and $a + b + c = 0$ Show that $4\left( {ax + by + cz} \right)^3 - 3\left( {ax + by + cz} \right)\left( {a^2 + b^2 + c^2 } \right)\left( {x^2 + y^2 + z^2 } \right) - 2\left( {b - c} \right)\left( {c - a} \right)\left( {a - b} \right)\left( {y - z} \right)\left( {z - x} \right)\left( {x - y} \right) = 54abcxyz$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69684 (x y z a b c : ℝ) (h1 : x + y + z = 0) (h2 : a + b + c = 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 * (b - c) * (c - a) * (a - b) * (y - z) * (z - x) * (x - y) = 54 * a * b * c * x * y * z   :=  by sorry

Source

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

View graph