Prove2Me

lean_workbook_plus_9116

Proved

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

and so, we only need to prove \n 6(x+y+z)2≥5∑x2+13∑xy, 6(x + y + z)^2 \ge 5\sum x^2 + 13\sum xy, which is equivalent to x2+y2+z2≥xy+yz+zx x^2 + y^2 + z^2 \ge xy + yz + zx (trivial).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9116 :
  ∀ x y z : ℝ, 6 * (x + y + z) ^ 2 ≥ 5 * (x ^ 2 + y ^ 2 + z ^ 2) + 13 * (x * y + y * z + z * x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph