Prove2Me

lean_workbook_plus_56485

Proved

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

This inequality is equivalent to ∑a+b+c2a+b+c≥94\sum \frac{a+b+c}{2a+b+c}\ge \frac{9}{4} . By CS we have \n (a+b+c)(∑12a+b+c)≥(a+b+c)(94(a+b+c))=94(a+b+c) (\sum \frac{1}{2a+b+c})\ge(a+b+c) (\frac{9}{4(a+b+c)})=\frac{9}{4}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56485 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → (a + b + c) * (1 / (2 * a + b + c) + 1 / (2 * b + a + c) + 1 / (2 * c + b + a)) ≥ 9 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph