lean_workbook_plus_61217

Disproved

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

Let $n\in \mathbb {N}$ and $n\geq 2$ . Prove that : $32\cdot n^{2n}\cdot (2n+1)>9\cdot (n+1)^{2n+1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61217 : ∀ n : ℕ, 2 ≤ n → 32 * n^(2 * n) * (2 * n + 1) > 9 * (n + 1)^(2 * n + 1)   :=  by sorry

Source