Prove2Me

lean_workbook_plus_15983

Disproved

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

If x,y x, y and zz are positive numbers, prove that \n

x+yz+y+zx+z+xy≥2(x+y+z)(1x+1y+1z).\frac{x+y}{z}+\frac{y+z}{x}+\frac{z+x}{y}\ge 2(x+y+z)(\frac{1}{ x}+\frac{1}{y }+\frac{1}{z }).

(WISCONSIN MATHEMATICS, SCIENCE & ENGINEERING TALENT SEARCH PROBLEM SET III (2011-2012) DECEMBER 2011)

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

View graph