A symmetric fourth-power inequality with coefficient thirteen

Proved

WorkbookSource.base_21127

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Show that for all non-negative $a$ , $b$ , and $c$ , we have

$13\left(a^4 + b^4 + c^4\right) + \left(a + b + c\right)^4 \ge 20\left(a^3b + a^3c + b^3c + b^3a + c^3a + c^3b\right)$

Source: InternLM Lean-Workbook, record lean_workbook_21127 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_21127 (a b c : ℝ) : 13 * (a ^ 4 + b ^ 4 + c ^ 4) + (a + b + c) ^ 4 ≥ 20 * (a ^ 3 * b + a ^ 3 * c + b ^ 3 * c + b ^ 3 * a + c ^ 3 * a + c ^ 3 * b)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_21127; Apache-2.0

View graph