lean_workbook_plus_2621

Disproved

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

I think it should be \n $\frac{2}{1+x^2}-\frac{2}{1+y^2}+\frac{3}{1+z^2} \le \frac{10}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2621 : ∀ x y z : ℝ, (2 / (1 + x ^ 2) - 2 / (1 + y ^ 2) + 3 / (1 + z ^ 2) : ℝ) ≤ 10 / 3   :=  by sorry

Source