Prove2Me

lean_workbook_plus_68932

Proved

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

Let a=y+z,b=x+z,c=x+y, x,y,z>0 a=y+z,b=x+z,c=x+y,\ x,y,z>0 . The inequality becomes \n 1y+z+1x+z+1x+y≤12(1x+1y+1z) \frac{1}{y+z}+\frac{1}{x+z}+\frac{1}{x+y}\leq\frac{1}{2}\left(\frac{1}{x}+\frac{1}{y}+\frac{1}{z}\right)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68932 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (1 / (x + y) + 1 / (y + z) + 1 / (z + x)) ≤ (1 / 2) * (1 / x + 1 / y + 1 / z)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph