lean_workbook_plus_47647

Proved

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

Let $x,y,z,u,v,w \in R$ ,prove that \n\n $(x-u)^2+(y-v)^2+(z-w)^2 \geq$ \n $\frac{1}{2}((x-z)(x-u-v+z)+(y-x)(y-v-w+x)+(z-y)(z-w-u+y))$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47647 (x y z u v w : ℝ) :
  (x - u) ^ 2 + (y - v) ^ 2 + (z - w) ^ 2 ≥
    1 / 2 * ((x - z) * (x - u - v + z) + (y - x) * (y - v - w + x) + (z - y) * (z - w - u + y))   :=  by sorry

Source

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

View graph