lean_workbook_plus_8114

Disproved

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

Prove that if $a^5-a^3+a=2$ , then $a^3$ is greater than 3 and less than 4.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8114 (a : ℝ) (h : a^5 - a^3 + a = 2) : 3 < a^3 ∧ a^3 < 4   :=  by sorry

Source