Prove2Me

Nonnegativity of a cyclic reciprocal sum

Proved
WorkbookSource.problem_26614

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that if a,b,c > 0 and abc=1, then 1(a+b+1)+1(b+c+1)+1(c+a+1)≥0\frac{1}{(a+b+1)} + \frac{1}{(b+c+1)} + \frac{1}{(c+a+1)}\geq0

Source: InternLM Lean-Workbook, record lean_workbook_26614 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_26614 (a b c : ℝ) (h1 : a > 0 ∧ b > 0 ∧ c > 0 ∧ a * b * c = 1) :
  1 / (a + b + 1) + 1 / (b + c + 1) + 1 / (c + a + 1) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_26614; Apache-2.0

View graph