A sextic polynomial has no real roots

Proved

WorkbookSource.plus_15828

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

lean-workbooksource-checked

Prove that the equation $x^6+x^5+x^4-x^3-x^2+1=0$ does not have any real solution.

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_15828 : ¬ (∃ x : ℝ, x^6 + x^5 + x^4 - x^3 - x^2 + 1 = 0)   :=  by sorry

Source