lean_workbook_plus_58504

Disproved

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

If $a$ , $b$ , $c$ are real numbers, prove that $\frac{a+b}{2b+c}+\frac{b+c}{2c+a}+\frac{c+a}{2a+b} \geq 2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58504 : ∀ a b c : ℝ, (a + b) / (2 * b + c) + (b + c) / (2 * c + a) + (c + a) / (2 * a + b) ≥ 2   :=  by sorry

Source