lean_workbook_plus_78642

Proved

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

Prove that the polynomial $8x^4 + 10x^3 - 21x^2 + 27$ is non-negative for all $x \geq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78642 (x : ℝ) (hx : x ≥ 0) : 8 * x^4 + 10 * x^3 - 21 * x^2 + 27 ≥ 0   :=  by sorry

Source