sum_of_reciprocals_primes_diverges
Provedanalytic-number-theorynumber-theoryproved
Sum of reciprocals of primes diverges: ∑ 1/p = ∞ (Euler 1737). Proved. This is equivalent to there being infinitely many primes.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sum_of_reciprocals_primes_diverges :
Filter.Tendsto (fun n : ℕ => ∑ p ∈ (Finset.range n).filter Nat.Prime, (1 : ℝ) / p)
Filter.atTop Filter.atTop := by
sorrySource