lean_workbook_plus_45124

Open

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

Prove that for positive reals $a,b,c,d,$ and $a+b+c+d=1$ ,

\sum_{cyc}\frac{a^3}{b+c} \ge \frac{1}{8}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45124 (hx: a + b + c + d = 1) (ha: a > 0 ∧ b > 0 ∧ c > 0 ∧ d > 0): a^3 / (b + c) + b^3 / (c + d) + c^3 / (d + a) + d^3 / (a + b) ≥ 1 / 8   :=  by sorry

Source

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

View graph