Prove2Me

Harmonic_Series_is_Divergent

Proved

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

analysisdivergenceproofwikiseries

The harmonic series sum_{n=1}^{infinity} 1/n diverges.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

theorem Harmonic_Series_is_Divergent : ¬ Summable (fun n : ℕ => (1 : ℝ) / (n + 1)) := by sorry
Source
https://proofwiki.org/wiki/Harmonic_Series_is_Divergent

View graph