Prove2Me

lean_workbook_plus_14046

Disproved

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

same conditions: xyxy+z+yzyz+x+xzxz+y≥1+4 xyz(y+z)(z+x)(x+y)\sqrt {{\frac {xy}{xy+z}}}+\sqrt {{\frac {yz}{yz+x}}}+\sqrt {{\frac {xz}{xz+y}}}\geq 1+4\,{\frac {xyz}{ \left( y+z \right) \left( z+x \right) \left( x+y \right) }}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14046 : ∀ x y z : ℝ, (Real.sqrt ((x * y) / (x * y + z)) + Real.sqrt ((y * z) / (y * z + x)) + Real.sqrt ((z * x) / (z * x + y)) ≥ 1 + 4 * (x * y * z) / ((y + z) * (z + x) * (x + y)))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph