Prove2Me

lean_workbook_plus_8373

Proved

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

For n=5n=5 then ineq is equivalent to

(x1−12x5)2+(x2−12x5)2+(x3−12x5)2+(x4−12x5)2≥0\left(x_1-\dfrac{1}{2}x_5\right)^2+\left(x_2-\dfrac{1}{2}x_5\right)^2+\left(x_3-\dfrac{1}{2}x_5\right)^2+\left(x_4-\dfrac{1}{2}x_5\right)^2\ge 0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8373 (x : ℕ → ℝ) : (x 1 - 1 / 2 * x 5) ^ 2 + (x 2 - 1 / 2 * x 5) ^ 2 + (x 3 - 1 / 2 * x 5) ^ 2 + (x 4 - 1 / 2 * x 5) ^ 2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph