lean_workbook_plus_64941

Proved

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

Find the $n$ th term of the sequence $\{a_{n}\}$ such that $a_{1}=\frac{1}{2},\ (n-1)a_{n-1}=(n+1){a_{n}}\ (n\geq 2).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64941 (n : ℕ) (a : ℕ → ℚ) (a1 : a 0 = 1 / 2) (a_rec : ∀ n, (n - 1) * a (n - 1) = (n + 1) * a n) : a n = 1 / (n * (n + 1))   :=  by sorry

Source

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

View graph