Mertens upper bound for prime reciprocals (Erdos 1210 analytic input)

Proved

Erdos1210.mertens_reciprocal_prime_upper

by junyihjy · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryerdos-problemsnumber-theoryprimes

Mertens' second theorem, upper-bound form: there exists an absolute constant C such that for every n ≥ 2, the sum of prime reciprocals below n satisfies ∑_{p<n} 1/p ≤ log(log(n)) + C. This is the analytic-number-theory input for Erdős Problem 1210 (it is not currently in Mathlib, which has only divergence of ∑ 1/p and Chebyshev θ/ψ bounds).

Preamble

import Mathlib

Formal statement

namespace Erdos1210

theorem mertens_reciprocal_prime_upper :
    ∃ C : ℝ, ∀ n : ℕ, 2 ≤ n →
      Finset.sum (Finset.filter Nat.Prime (Finset.range n)) (fun p => 1 / (p : ℝ)) ≤
        Real.log (Real.log (n : ℝ)) + C := by sorry

end Erdos1210

Source

Mertens' second theorem; analytic input for Erdős Problem #1210, https://www.erdosproblems.com/1210.

View graph