Prove2Me

lean_workbook_plus_82018

Disproved

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

Prove that:\nx3(xy+xz−yz)(y−z)2+y3(xy+yz−zx)(z−x)2+z3(zx+yz−xy)(x−y)2≥0x^3(xy+xz-yz)(y-z)^2+y^3(xy+yz-zx)(z-x)^2+z^3(zx+yz-xy)(x-y)^2 \geq 0

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

View graph