Prove2Me

lean_workbook_plus_59576

Proved

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

Let x,y,z,u,v,w∈Rx,y,z,u,v,w \in R ,prove that \n\n 1.(x−u)2+(y−v)2+(z−w)2≥1.(x-u)^2+(y-v)^2+(z-w)^2 \geq \n 12((x−z)(x−u−v+z)+(y−x)(y−v−w+x)+(z−y)(z−w−u+y)) \frac{1}{2}((x-z)(x-u-v+z)+(y-x)(y-v-w+x)+(z-y)(z-w-u+y)) \n\n 2.(x−z)(x−w)+(y−x)(y−u)+(z−y)(z−v)≥2((x−u)(u−z)+(y−v)(v−x)+(w−y)(z−w))2.(x-z)(x-w)+(y-x)(y-u)+(z-y)(z-v)\geq 2((x-u)(u-z)+(y-v)(v-x)+(w-y)(z-w)) \n\n 3.(x−z)(2x−u−z)+(y−x)(2y−v−x)+(z−y)(2z−w−y)≥2((v−w)(u−v)+(w−u)(v−w)+(w−u)(u−v))3.(x-z)(2x-u-z)+(y-x)(2y-v-x)+(z-y)(2z-w-y) \geq 2((v-w)(u-v)+(w-u)(v-w)+(w-u)(u-v))

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59576 :  ∀ 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