Prove2Me

lean_workbook_plus_57068

Proved

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

Prove that (x+y+z)(xab+ybc+zca)≤(x2+y2+z2)(a2+b2+c2)(x+y+z)(xab+ybc+zca)\leq(x^2+y^2+z^2)(a^2+b^2+c^2) For all reals a,b,c,x,y,z. Can it be proved by Cauchy or Holder?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57068 (x y z a b c : ℝ) : (x + y + z) * (x * a * b + y * b * c + z * c * a) ≤ (x ^ 2 + y ^ 2 + z ^ 2) * (a ^ 2 + b ^ 2 + c ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph