Prove2Me

lean_workbook_plus_74766

Proved

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

Applying AM-GM, we get \n 4(b2+bc+c2)(ab+bc+ca)≤(ab+bc+ca+b2+bc+c2)2=(b+c)2(a+b+c)24\left( {{b^2} + bc + {c^2}} \right)\left( {ab + bc + ca} \right) \le {\left( {ab + bc + ca + {b^2} + bc + {c^2}} \right)^2} = {(b + c)^2}{(a + b + c)^2}

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

View graph