lean_workbook_plus_27711

Disproved

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

Prove that $\frac{1}{1+{y}^{2}}\leq \frac{27}{50}\left(2-y \right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27711 : ∀ y : ℝ, (1 / (1 + y ^ 2) : ℝ) ≤ (27 / 50) * (2 - y)   :=  by sorry

Source