Prove2Me

lean_workbook_plus_1824

Disproved

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

if\n x2+y2+z2=1x^2+y^2+z^2=1 ,then:\n\n x+y+z1+y2x2≥92(yz+1)2(zx+1)2(yz+1)2(zx+1)2+(zx+1)2(xy+1)2+(xy+1)2(yz+1)2\frac{x+y+z}{1+y^2x^2}\geq \frac{9}{2}\frac{(yz+1)^2(zx+1)^2}{(yz+1)^2(zx+1)^2+(zx+1)^2(xy+1)^2+(xy+1)^2(yz+1)^2}

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

View graph