lean_workbook_plus_63390

Disproved

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

Squaring the original inequality we get it is equivalent to $\frac{1}{1+x^2}+\frac{1}{1+y^2} + \frac{2}{\sqrt{(x^2+1)(y^2+1)}} \le \frac{4}{1+xy}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63390 :
  ∀ x y : ℝ,
    1 / (1 + x^2) + 1 / (1 + y^2) + 2 / Real.sqrt ((x^2 + 1) * (y^2 + 1)) ≤ 4 / (1 + x * y)   :=  by sorry

Source

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

View graph