Prove2Me

lean_workbook_plus_53247

Disproved

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

Prove the inequality \n

a+ba+b+2c+b+cb+c+2a+a+ca+c+2b≥32\frac{a+b}{a+b+2c}+\frac{b+c}{b+c+2a}+\frac{a+c}{a+c+2b}\geq\frac{3}{2}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53247 : ∀ a b c : ℝ, (a + b) / (a + b + 2 * c) + (b + c) / (b + c + 2 * a) + (a + c) / (a + c + 2 * b) ≥ 3 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph