lean_workbook_plus_50024

Proved

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

Let $S=x^2+y^2+z^2-xy-yz-zx$ , then $2S=(x-y)^2+(y-z)^2+(z-x)^2$ .\nLet $|x-y|\geq|y-z|\geq|z-x|$ . Because there are no two equal numbers, $|z-x|>0 \Rightarrow |y-z|\geq|z-x|\geq1$ .\nLet $|y-z|=|z-x|=1 \Rightarrow |x-y|=2$ , so minimum value of $2S$ is greater than or equal to $1+1+2^2=6$ but for $y=3, z=2, x=1$ we get that value so minimum value is $S=3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50024  (x y z : ℝ)
  (h₀ : 0 < abs (x - y))
  (h₁ : 0 < abs (y - z))
  (h₂ : 0 < abs (z - x))
  (h₃ : abs (x - y) ≥ abs (y - z))
  (h₄ : abs (y - z) ≥ abs (z - x))
  (h₅ : abs (z - x) ≥ 1) :
  3 ≤ x^2 + y^2 + z^2 - x * y - y * z - z * x   :=  by sorry

Source

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

View graph