Prove2Me

lean_workbook_plus_25763

Proved

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

Prove x2+y2+z2≥xy+yz+zxx^2+y^2+z^2 \geq xy+yz+zx using the rearrangement inequality.

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

View graph