Prove2Me

lean_workbook_plus_18771

Disproved

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

prove that \n1x(1+x)(x+yz)+1y(y+xz)(y+1)+1(z+1)z(z+xy)≥6 1(xy+1)(yz+1)(xz+1){\frac {1}{x \left( 1+x \right) \left( x+yz \right) }}+{\frac {1}{y\left( y+xz \right) \left( y+1 \right) }}+{\frac {1}{ \left( z+1 \right) z \left( z+xy \right) }}\geq 6\,{\frac {1}{ \left( xy+1 \right) \left( yz+1 \right) \left( xz+1 \right) }}

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

View graph