Prove2Me

lean_workbook_plus_61831

Disproved

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

prove that: 3≥1+x3−yz+1+y3−zx+1+z3−xy≥2+19(xy+zx+yz)+23x2y2z23\geq \frac{1+x}{3-yz}+\frac{1+y}{3-zx}+\frac{1+z}{3-xy} \geq 2+\frac{1}{9}(xy+zx+yz)+\frac{2}{3}x^2y^2z^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61831 : ∀ x y z : ℝ, 3 ≥ (1 + x) / (3 - y * z) + (1 + y) / (3 - z * x) + (1 + z) / (3 - x * y) ∧ (1 + x) / (3 - y * z) + (1 + y) / (3 - z * x) + (1 + z) / (3 - x * y) ≥ 2 + 1 / 9 * (x * y + z * x + y * z) + 2 / 3 * x ^ 2 * y ^ 2 * z ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph