lean_workbook_plus_44151

Open

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

$\frac {1}{997} + \frac {1}{998} + ... + \frac {1}{1995} < 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44151 : ∑ k in Finset.Icc (997 : ℕ) 1995, (1 : ℝ) / k < 1   :=  by sorry

Source