lean_workbook_plus_82769

Proved

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

Let $a$ be positive real numbers such that $a^3-a-2=0$ . Prove that $\sqrt[4]{5}<a<2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82769 (a : ℝ) (ha : a^3 - a - 2 = 0) : (5:ℝ)^(1/4) < a ∧ a < 2   :=  by sorry

Source