Prove2Me

lean_workbook_plus_40974

Open

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

Prove that ∑i=1641i<6.4\sum_{i=1}^{64}\frac{1}{i} < 6.4.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40974 : ∑ i in Finset.Icc (1 : ℕ) 64, (1 : ℝ) / i < 6.4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph