lean_workbook_plus_75

Proved

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

It's equivalent to \n\n $ab+bc+ca\le 3abc+2(a^3+b^3+c^3)$ \n\n $\Leftrightarrow 2(a^3+b^3+c^3)+3abc\ge (ab+bc+ca)(a+b+c)=\sum ab(a+b)+3abc$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75 {a b c : ℝ} (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) : 2 * (a ^ 3 + b ^ 3 + c ^ 3) + 3 * a * b * c ≥ (a * b + b * c + c * a) * (a + b + c)   :=  by sorry

Source

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

View graph