lean_workbook_plus_36233

Disproved

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

Prove the inequality\n $a^4+b^4+c^4+abc(a+b+c)\\leq2(a^2b^2+b^2c^2+c^2a^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36233 : ∀ a b c : ℝ, a^4 + b^4 + c^4 + a * b * c * (a + b + c) ≤ 2 * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2)   :=  by sorry

Source