← Formalpedia
lean_workbook_plus_28991 Disproved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
3 2 + a b a + b + b c b + c + c a c + a ≥ a b + b c + c a ⇔ a + b + c 2 + ∑ c y c a b a + b ≥ 3 ( a b + a c + b c ) a + b + c ⇔ \frac{3}{2}+\frac{ab}{a+b}+\frac{bc}{b+c}+\frac{ca}{c+a}\ge ab+bc+ca \Leftrightarrow \frac{a+b+c}{2}+\sum_{cyc}\frac{ab}{a+b}\geq\frac{3(ab+ac+bc)}{a+b+c} \Leftrightarrow 2 3 + a + b ab + b + c b c + c + a c a ≥ ab + b c + c a ⇔ 2 a + b + c + ∑ cy c a + b ab ≥ a + b + c 3 ( ab + a c + b c ) ⇔
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_28991 : ∀ a b c : ℝ, a + b + c > 0 → 3 / 2 + a * b / (a + b) + b * c / (b + c) + c * a / (c + a) ≥ a * b + b * c + c * a := by sorry View graph