Lean-Workbook Syntax 39501: Four reciprocal-square partial-sum bounds

Proved

WorkbookSyntax.plus_39501

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

lean-workbookrepaired-notationsource-checked

For $n\in\{1,2,3,4\}$ , $\sum_{k=1}^{n}1/k^2<5/3$ .

Source: Lean-Workbook row lean_workbook_plus_39501 (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.Analysis.Complex.Basic
import Mathlib.Algebra.BigOperators.Intervals

Formal statement

theorem WorkbookSyntax.plus_39501 : ∀ n : ℕ, n ∈ ({1, 2, 3, 4} : Finset ℕ) → ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / k ^ 2 < 5 / 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_39501; immutable original Prove2Me node 7b7d9270-3f08-4e64-bf54-85615acfc0f6

View graph