Lean-Workbook Syntax 60317: A finite telescoping reciprocal sum

Proved

WorkbookSyntax.plus_60317

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

$\sum_{k=1}^{49}1/[k(k+1)]=49/50$ . The Lean declaration also includes $k=0$ , whose term is zero under totalized division, so the finite sum has the same value.

Source: Lean-Workbook row lean_workbook_plus_60317 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic

Formal statement

theorem WorkbookSyntax.plus_60317 :
  ∑ k ∈ (Finset.range 50), (1 : ℝ) / (k * (k + 1)) = 49 / 50   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_60317; immutable original Prove2Me node 326f22e4-0be6-4f1e-ba00-7b31e5bedbb4

View graph