lean_workbook_plus_59787

Proved

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

Let $a, b, c \geq0$ . Prove that \n

\frac{1}{8} \cdot \frac{(2+a) (2+b) (2+c)} {(1+a) (1+b) (1+c)} \geq \frac{4-a-b-c} {4+a+b+c}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59787 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : (1 / 8 * (2 + a) * (2 + b) * (2 + c) / ((1 + a) * (1 + b) * (1 + c))) ≥ (4 - a - b - c) / (4 + a + b + c)   :=  by sorry

Source

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

View graph