Exact reciprocal sum from a bilinear recurrence

Proved

WorkbookSource.plus_54508

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksequencessource-checked

Let $a_0=3$ and suppose the real sequence satisfies

(3-a_{n+1})(6+a_n)=18\qquad(n\geq0).

Then

\sum_{k=0}^{12}\frac1{a_k}=\frac{16369}{3}.

The statement gives the exact reciprocal sum for the specified nonlinear recurrence.

Formalization Note: The source proposition is retained; obsolete summation notation is updated for Lean 4.33.1.

Preamble

import Mathlib
open scoped BigOperators

Formal statement

theorem WorkbookSource.plus_54508 (a : ℕ → ℝ) (a0 : a 0 = 3) (a_rec : ∀ n, (3 - a (n + 1)) * (6 + a n) = 18) : ∑ k ∈ Finset.range 13, (1 / a k) = 16369 / 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_54508; Apache-2.0

View graph