Prove2Me

lean_workbook_plus_3982

Proved

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

We have a well-known inequality (a+b+c)(a2+b2+c2)≥3(a2b+b2c+c2a)⇔a(a−b)2+b(b−c)2+c(c−a)2≥0 \begin{array}{l} \left( {a + b + c} \right)\left( {{a^2} + {b^2} + {c^2}} \right) \ge 3\left( {{a^2}b + {b^2}c + {c^2}a} \right) \Leftrightarrow a{\left( {a - b} \right)^2} + b{\left( {b - c} \right)^2} + c{\left( {c - a} \right)^2} \ge 0 \end{array}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3982 (a b c : ℝ) : (a + b + c) * (a ^ 2 + b ^ 2 + c ^ 2) ≥ 3 * (a ^ 2 * b + b ^ 2 * c + c ^ 2 * a) ↔ a * (a - b) ^ 2 + b * (b - c) ^ 2 + c * (c - a) ^ 2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph