lean_workbook_plus_39501

Open

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

Check that $\sum_{k=1}^n \frac {1} {k^2} < \frac {5} {3}$ , for $n=1,2,3,4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source