lean_workbook_plus_5943

Proved

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

The general term in the sequence is $\frac{2^k k}{(k+1)(k+2)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5943 (f : ℕ → ℝ) (k : ℕ) (h₁ : f k = 2 ^ k * k / ((k + 1) * (k + 2))) : f k = 2 ^ k * k / ((k + 1) * (k + 2))   :=  by sorry

Source

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

View graph