Prove2Me

lean_workbook_plus_60010

Proved

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

prove that: (x+y−z)(z+x−y)(x−y)(x−z)+(y+z−x)(x+y−z)(y−z)(y−x)+(z+x−y)(y+z−x)(z−x)(z−y)≥0(x+y-z)(z+x-y)(x-y)(x-z)+(y+z-x)(x+y-z)(y-z)(y-x)+(z+x-y)(y+z-x)(z-x)(z-y)\geq 0

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

View graph