lean_workbook_plus_2785Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)↔ \leftrightarrow↔ (a+b+c)2(ab+bc+ca)≥6abc(a+b+c)+(a2+b2+c2)(ab+bc+ca) \left(a+b+c\right)^2\left( ab+bc+ca\right)\geq 6abc\left(a+b+c\right)+\left(a^2+b^2+c^2\right)\left(ab+bc+ca\right)(a+b+c)2(ab+bc+ca)≥6abc(a+b+c)+(a2+b2+c2)(ab+bc+ca)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_2785 {a b c : ℝ} : (a + b + c) ^ 2 * (a * b + b * c + c * a) ≥ 6 * a * b * c * (a + b + c) + (a ^ 2 + b ^ 2 + c ^ 2) * (a * b + b * c + c * a) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph