A quartic polynomial bound under a coefficient constraint

Proved

WorkbookSource.plus_50717

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $a, b, c, d, x\in \mathbb{R}$ and $a^{2}+c^{2}\leq 4b$ . Prove that $x^{4}+ax^{3}+bx^{2}+cx+1\geq 0$ .

Source: InternLM Lean-Workbook, record lean_workbook_plus_50717 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_50717 (a b c d x : ℝ) (a2c2_leq_4b : a^2 + c^2 ≤ 4*b) : x^4 + a*x^3 + b*x^2 + c*x + 1 ≥ 0   :=  by sorry

Source