lean_workbook_plus_7776

Proved

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

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7776 : ¬ ∃ x : ℝ, x^6 + x^5 + x^4 - x^3 - x^2 + 1 = 0   :=  by sorry

Source