lean_workbook_plus_16687

Disproved

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

This is equivalent to show that $32a^{5}+32a^{4}-16a^{3}-16a^{2}+9a-1\geq 0$ for a $\in$ [0,1]

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16687 : ∀ a ∈ Set.Icc (0:ℝ) 1, 32*a^5 + 32*a^4 - 16*a^3 - 16*a^2 + 9*a - 1 ≥ 0   :=  by sorry

Source