Finite endpoint certificate for the reciprocal-prime estimate below 512

Proved

TaoFivePrimes.mertens_reciprocal_endpoint_certificate_511

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

Let $B=\gamma+\sum_p(\log(1-1/p)+1/p)$ be the Meissel–Mertens constant. For every integer $2\le n\le511$ ,

\sum_{p\le n}\frac1p\le\log\log n+B+\frac4{\log^3(n+1)}.

The use of $n+1$ in the correction term makes this a sufficient finite endpoint certificate for every real point in $[n,n+1)$ . This is a concrete 510-case numerical certificate, not an assertion that the finite verification has been completed.

Preamble

import Mathlib

Formal statement

theorem TaoFivePrimes.mertens_reciprocal_endpoint_certificate_511 (n : ℕ) (hn : 2 ≤ n) (hN : n ≤ 511) :
    (∑ p ∈ Nat.primesLE n, 1 / (p : ℝ)) ≤
      Real.log (Real.log (n : ℝ)) +
        (Real.eulerMascheroniConstant +
          ∑' p : Nat.Primes, (Real.log (1 - 1 / (p : ℝ)) + 1 / (p : ℝ))) +
        4 / (Real.log ((n : ℝ) + 1)) ^ 3 := by sorry

Source

Finite endpoint strengthening, introduced for the reduction of TaoFivePrimes.mawia_reciprocal_sum_upper_bound_small. The parent is the Mawia reciprocal-prime estimate; this numerical certificate is an auxiliary obligation, not a quoted theorem from Mawia.

View graph