by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let a,b,c,d≥0 ,prove that: \n\n (b+c)(c+d)(b+d)a3+(c+d)(d+a)(c+a)b3+(d+a)(a+b)(b+d)c3+(a+b)(b+c)(c+a)d3≥21 \n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39698 : ∀ a b c d : ℝ, a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 ∧ d ≥ 0 → a^3 / (b + c) / (c + d) / (b + d) + b^3 / (c + d) / (d + a) / (c + a) + c^3 / (d + a) / (a + b) / (b + d) + d^3 / (a + b) / (b + c) / (c + a) ≥ 1 / 2 := by sorry