lean_workbook_plus_1453

Proved

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

Let $a,b,c \ge 0$ . prove that \n\n $abc + \frac {13}{3} (a + b + c)^3 \ge \frac {25}{2}(a + b)(b + c)(c + a)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1453 (a b c : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) : a * b * c + (13/3) * (a + b + c) ^ 3 ≥ (25/2) * (a + b) * (b + c) * (c + a)   :=  by sorry

Source

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

View graph