lean_workbook_plus_76557

Proved

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

prove that $(a+b+c+d)^3 \geq 16(abc + bcd + acd + adb)$ if $a,b,c,d$ are non negative numbers

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph