lean_workbook_plus_23371

Proved

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

Let $a,\,b,\,c$ are non-negative real numners. Prove that $a^4+b^4+c^4 \geqslant abc(a+b+c)+ \frac{14}{5} \cdot ab (a-b)^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23371 : ∀ a b c : ℝ, a^4 + b^4 + c^4 ≥ a * b * c * (a + b + c) + (14 / 5) * a * b * (a - b)^2   :=  by sorry

Source