lean_workbook_plus_60852

Proved

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

$x,y,z,u,v,w$ are real numbers,prove that: \n\n $(x-z)(v-z)+(y-x)(w-x)+(u-y)(z-y)-2(u-v)v-2(v-w)w-2(w-u)u\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60852 (x y z u v w : ℝ) :
  (x - z) * (v - z) + (y - x) * (w - x) + (u - y) * (z - y) - 2 * (u - v) * v - 2 * (v - w) * w - 2 * (w - u) * u ≥ 0   :=  by sorry

Source

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

View graph