Mertens limit with the exact Euler-product constant

Proved

TaoFivePrimes.reciprocal_prime_mertens_limit

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorymertens-theorem

The reciprocal-prime sum has the limit

\lim_{x\to\infty}\left(\sum_{p\le x}\frac1p-\log\log x\right)=\gamma+\sum_p\left(\log(1-1/p)+1/p\right).

The right side explicitly identifies the Meissel–Mertens constant through an absolutely convergent prime series. Unlike an existential version of Mertens' second theorem, this statement identifies the constant needed to convert finite Abel summation into the exact theta-tail identity. The accompanying proof adapts the complete formal proof of Mertens' second theorem and constant identification from the PrimeNumberTheoremAnd project.

Preamble

import Mathlib
open Filter Topology

Formal statement

theorem TaoFivePrimes.reciprocal_prime_mertens_limit :
    Tendsto (fun x : ℝ =>
      (∑ p ∈ Nat.primesLE ⌊x⌋₊, 1 / (p : ℝ)) - Real.log (Real.log x))
      atTop (nhds (Real.eulerMascheroniConstant +
        ∑' p : Nat.Primes, (Real.log (1 - 1 / (p : ℝ)) + 1 / (p : ℝ)))) := by sorry

Source

PrimeNumberTheoremAnd, revision 55270df807213fc3584523d09e0311d7dc073ff5, PrimeNumberTheoremAnd/IEANTN/Mertens.lean, Mertens.E₂p.bound' and Mertens.M.eq. https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/55270df807213fc3584523d09e0311d7dc073ff5/PrimeNumberTheoremAnd/IEANTN/Mertens.lean. Apache License 2.0.

View graph