Prove2Me

lean_workbook_plus_70401

Proved

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

Let a,b,c>0.a,b,c>0. Prove that a2b+a+bc+a+b+ca+b≥52\frac{ a}{2b}+\frac{a+b}{c+a}+\frac{b+c}{a+b} \geq\frac{5}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70401 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a / (2 * b) + (a + b) / (c + a) + (b + c) / (a + b)) ≥ 5 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph