lean_workbook_plus_31342Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)1a+b+1+1b+c+1+1c+a+1≥1⇔2(a+b+c+1)≥(a+b)(a+c)(b+c)\frac{1}{a+b+1}+\frac{1}{b+c+1}+\frac{1}{c+a+1}\ge1\Leftrightarrow 2(a+b+c+1)\geq(a+b)(a+c)(b+c)a+b+11+b+c+11+c+a+11≥1⇔2(a+b+c+1)≥(a+b)(a+c)(b+c)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_31342 : ∀ a b c : ℝ, (1 / (a + b + 1) + 1 / (b + c + 1) + 1 / (c + a + 1) ≥ 1 ↔ 2 * (a + b + c + 1) ≥ (a + b) * (a + c) * (b + c)) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph