Prove2Me

lean_workbook_plus_55498

Proved

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

With conditions x,y,z>0x,y,z>0 and xy+yz+zx=1xy+yz+zx=1 . we have \n 1x+y+1y+z+1z+x−52=3∑x(y+z−1)2+4(x+y+z−2)2+xyz4(y+z)(z+x)(x+y)≥0\frac{1}{x+y} +\frac{1}{y+z} +\frac{1}{z+x}-\frac{5}{2}=\frac{3\sum{x(y+z-1)^2}+4(x+y+z-2)^2+xyz}{4(y+z)(z+x)(x+y)}\ge{0}

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

View graph