lean_workbook_plus_23294

Proved

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

Determine whether the series $\sum_{n=2}^{\infty} a_n$ is absolutely convergent, conditionaly convergent or divergent. Given $a_n=\frac{1+n+n^2}{\sqrt{1+n^2+n^6}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23294 (n : ℕ) (hn : 2 ≤ n) (a_n : ℝ) (ha_n : a_n = (1 + n + n^2) / (Real.sqrt (1 + n^2 + n^6))) : ∃ l, ∑' n : ℕ, a_n = l   :=  by sorry

Source

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

View graph