lean_workbook_plus_9060

Disproved

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

Observe that $-\frac{27}{392}\left(a-\frac{1}{3}\right)+\frac{9}{28} \geq \frac{1}{a^2+3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9060 : ∀ a : ℝ, (-(27 / 392) * (a - 1 / 3) + 9 / 28) ≥ 1 / (a ^ 2 + 3)   :=  by sorry

Source