lean_workbook_plus_45633

Disproved

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

prove that: $2\geq {\frac {1+xy}{2\,{z}^{2}+1+xy}}+{\frac {1+yz}{2\,{x}^{2}+1+yz}}+{\frac {1+xz}{2\,{y}^{2}+1+xz}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45633 : ∀ x y z : ℝ, (2 : ℝ) ≥ (1 + x * y) / (2 * z ^ 2 + 1 + x * y) + (1 + y * z) / (2 * x ^ 2 + 1 + y * z) + (1 + z * x) / (2 * y ^ 2 + 1 + z * x)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph