lean_workbook_plus_5040

Disproved

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

Let $a = 1 + x,\ b = 1 - x$ where $x \geq 0$ . The problem becomes: $14 + \sqrt{2 - x^2} \geq |x^4-9x^2|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5040 : ∀ x ≥ 0, 14 + Real.sqrt (2 - x ^ 2) ≥ |x ^ 4 - 9 * x ^ 2|   :=  by sorry

Source