lean_workbook_plus_68004

Proved

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

We have \n $\left( {{a^2} + 2bc} \right)\left( {{b^2} + 2ca} \right)\left( {{c^2} + 2ab} \right) + \frac{(a^2+b^2+c^2)^3}{4}=\frac{1}{12}(a^2+b^2+c^2)(a+b+c)^4+\frac{1}{27}\prod{(a+b-2c)^2}+\frac{1}{54}(a+b+c)^6\ge{0}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68004 (a b c : ℝ) :
  (a^2 + 2 * b * c) * (b^2 + 2 * c * a) * (c^2 + 2 * a * b) + (a^2 + b^2 + c^2)^3 / 4 ≥
  (a^2 + b^2 + c^2) * (a + b + c)^4 / 12 + (a + b - 2 * c)^2 * (b + c - 2 * a)^2 * (c + a - 2 * b)^2 / 27 + (a + b + c)^6 / 54   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph