Prove2Me

A reciprocal pairwise-sum lower bound

Proved
WorkbookSource.base_4819

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

lean-workbooksource-checked

Prove that for all positive real numbers x,y,zx, y, z the following inequality holds:

1x+y+1y+z+1z+x≥15(x+y+z)2(x2+y2+z2)+8(xy+yz+zx).\frac 1{x + y} + \frac 1{y + z} + \frac 1{z + x} \ge \frac {15 (x + y + z)}{2(x^2 + y^2 + z^2) + 8 (xy + yz + zx)}.

Source: InternLM Lean-Workbook, record lean_workbook_4819 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_4819 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (1 / (x + y) + 1 / (y + z) + 1 / (z + x)) ≥ 15 * (x + y + z) / (2 * (x ^ 2 + y ^ 2 + z ^ 2) + 8 * (x * y + y * z + z * x))  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_4819; Apache-2.0

View graph