lean_workbook_plus_74946

Proved

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

$\frac { 1}{a + b} + \frac { 1}{b + c} + \frac { 1}{c + a}\geq \frac {9}{2(a + b + c)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74946 {a b c : ℝ} (ha : a > 0) (hb : b > 0) (hc : c > 0) : 1 / (a + b) + 1 / (b + c) + 1 / (c + a) ≥ 9 / (2 * (a + b + c))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph