lean_workbook_plus_9731

Proved

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

For all integers $n$ , $|n| > 2$ , $(2n^2+n-2)^2<4(n^4+n^3+1) < (2n^2+n)^2\,.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9731 (n : ℤ) (hn : abs n > 2) : (2 * n ^ 2 + n - 2) ^ 2 < 4 * (n ^ 4 + n ^ 3 + 1) ∧ 4 * (n ^ 4 + n ^ 3 + 1) < (2 * n ^ 2 + n) ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph