lean_workbook_plus_43460

Disproved

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

It is well known that $4(a^2b+b^2c+c^2a+abc) \le \frac{16}{27}(a+b+c)^3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43460 : ∀ a b c : ℝ, 4 * (a ^ 2 * b + b ^ 2 * c + c ^ 2 * a + a * b * c) ≤ (16 / 27) * (a + b + c) ^ 3   :=  by sorry

Source