Prove2Me

lean_workbook_plus_31968

Proved

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

∑cyc(x3+2x2y−3x2z)≥0⇔∑cyc(2x3+4x2y−6x2z)≥0⇔\sum_{cyc}(x^3+2x^2y-3x^2z)\geq0\Leftrightarrow\sum_{cyc}(2x^3+4x^2y-6x^2z)\geq0\Leftrightarrow ⇔∑cyc(2x3−x2y−x2z)≥5∑cyc(x2z−x2y)⇔\Leftrightarrow\sum_{cyc}(2x^3-x^2y-x^2z)\geq5\sum_{cyc}(x^2z-x^2y)\Leftrightarrow ⇔∑cyc(2x3−x2y−x2z)≥5(x−y)(y−z)(z−x)\Leftrightarrow\sum_{cyc}(2x^3-x^2y-x^2z)\geq5(x-y)(y-z)(z-x) .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31968 : ∀ x y z : ℝ, (x ^ 3 + y ^ 3 + z ^ 3 + 2 * (x ^ 2 * y + y ^ 2 * z + z ^ 2 * x) - 3 * (x ^ 2 * z + y ^ 2 * x + z ^ 2 * y) ≥ 0 ↔ 2 * (x ^ 3 + y ^ 3 + z ^ 3) + 4 * (x ^ 2 * y + y ^ 2 * z + z ^ 2 * x) - 6 * (x ^ 2 * z + y ^ 2 * x + z ^ 2 * y) ≥ 0)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph