lean_workbook_plus_17334

Proved

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

Prove the convergence of the series: $u_n = \frac{1}{(4n+1)(4n+2)(4n+3)(4n+4)}$ , for all $n \in \mathbb{N}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17334 (u : ℕ → ℝ) (h : ∀ n, u n = 1 / (4 * n + 1) / (4 * n + 2) / (4 * n + 3) / (4 * n + 4)) : ∃ l, ∑' n : ℕ, u n = l   :=  by sorry

Source

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

View graph