lean_workbook_plus_279

Proved

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

If $a,b,c,d$ are nonnegative real numbers, then $(a + b + c + d)^{3}\\geq 4[a(c + d)^{2} + b(d + a)^{2} + c(a + b)^{2} + d(b + c)^{2}]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_279 (a b c d : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) : (a + b + c + d) ^ 3 ≥ 4 * (a * (c + d) ^ 2 + b * (d + a) ^ 2 + c * (a + b) ^ 2 + d * (b + c) ^ 2)   :=  by sorry

Source

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

View graph