Prove2Me

lean_workbook_plus_34922

Proved

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

We know that ∑x2≥∑xy⟺∑(x−y)2≥0, ∀x,y,z∈R\sum x^2\geq \sum xy\Longleftrightarrow \sum(x-y)^2\geq 0,~ \forall x,y,z\in\mathbb{R}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34922 (x y z: ℝ) : x ^ 2 + y ^ 2 + z ^ 2 ≥ x * y + y * z + z * x ↔ (x - y) ^ 2 + (y - z) ^ 2 + (z - x) ^ 2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph