lean_workbook_plus_13790

Proved

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

Prove that for real numbers $a, b, c, d$ , the inequality $a^3(b + c + d) + b^3(a + c + d) + c^3(a + b + d) + d^3(a + b + c) \leq \frac{3}{4}(a^2 + b^2 + c^2 + d^2)^2$ holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13790 (a b c d : ℝ) : a ^ 3 * (b + c + d) + b ^ 3 * (a + c + d) + c ^ 3 * (a + b + d) + d ^ 3 * (a + b + c) ≤ (3 / 4 : ℝ) * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) ^ 2   :=  by sorry

Source

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

View graph