Dusart's explicit upper bound for $\sum_{p\le x}1/p$

Open

QRHLittlewood.dusart_reciprocal_primes

by @bwdaugherty · 1 vote · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theory

Let $\gamma$ be the Euler–Mascheroni constant and let

B=\gamma+\sum_{p}\Big(\log\Big(1-\frac1p\Big)+\frac1p\Big)

be Mertens' constant, the sum running over all primes. For every real $x\ge10372$ ,

\sum_{p\le x}\frac1p-\log\log x-B\ \le\ \frac{1}{10\log^2x}+\frac{4}{15\log^3x}.

This is the explicit form of Mertens' second theorem used to bound smoothed sums over primes.

Status note (2026-10-17) The release Dusart v2.0.0, doi:10.5281/zenodo.23432990 proves this bound in Lean 4 from the Chebyshev estimate for $t\ge3584912846=\lfloor e^{22}\rfloor$ alone (Dusart.dusart_reciprocal_primes_of_chebyshev_large).

Status note (2026-10-19) The release Dusart v3.0.0, doi:10.5281/zenodo.23463154 proves this bound in Lean 4 with a single published table row as the only hypothesis, $|\theta(t)-t|<0.15952\,t/\log^2t$ for $t>5\cdot10^6$ (Broadbent, Kadiri, Lumley, Ng and Wilk, Math. Comp. 90 (2021), Theorem 1 with $k=2$ , Table 15, row $\log X_0=\log(5\cdot10^6)$ ) (Dusart.dusart_reciprocal_primes_of_bklnw; axioms propext, Classical.choice, Quot.sound only). With that published theorem the bound holds unconditionally as mathematics; the row itself is not formalized, so on this platform the entry stays reduced to the Chebyshev estimate.

Preamble

import Mathlib.NumberTheory.Harmonic.EulerMascheroni
import Mathlib.NumberTheory.LSeries.DirichletContinuation

open Real

Formal statement

namespace QRHLittlewood

theorem dusart_reciprocal_primes (x : ℝ) (hx : 10372 ≤ x) :
    (∑ p ∈ Finset.filter Nat.Prime (Finset.range (⌊x⌋₊ + 1)), (1 : ℝ) / p) - Real.log (Real.log x) -
        (Real.eulerMascheroniConstant + ∑' p : Nat.Primes, (Real.log (1 - 1 / (p : ℝ)) + 1 / (p : ℝ))) ≤
      1 / (10 * Real.log x ^ 2) + 4 / (15 * Real.log x ^ 3) := by sorry

end QRHLittlewood

Source

P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442 (2010), Theorem 6.10 (upper bound).

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Statement. For every real number $x\ge 10372$ ,

\sum_{\substack{p\ \text{prime}\\ p\le x}}\frac1p\;-\;\log\log x\;-\;B\;\le\;\frac{1}{10(\log x)^2}+\frac{4}{15(\log x)^3},

where $\log$ is the natural logarithm and

B=\gamma+\sum_{p\ \text{prime}}\Bigl(\log\Bigl(1-\frac1p\Bigr)+\frac1p\Bigr),

with $\gamma$ the Euler–Mascheroni constant.

Details.

The finite sum runs over primes $p$ in $\{0,1,\dots,\lfloor x\rfloor\}$ , i.e. exactly the primes $p\le x$ (here $\lfloor x\rfloor\ge 10372$ is the usual floor since $x>0$ ).
The infinite sum over all primes is an unconditional (summability-based) sum; in Mathlib such a sum is defined to be $0$ if the family is not summable. The terms $\log(1-1/p)+1/p$ are negative and of size about $-1/(2p^2)$ , so this junk convention would only matter if the family failed to be summable.
For $x\ge 10372$ , $\log x>9$ , so all logarithms and denominators are genuine (no junk values).
This is a one-sided bound: only an upper bound on $\sum_{p\le x}1/p-\log\log x-B$ is asserted; no lower bound is claimed. The difference may be negative.
No hypotheses other than $x\ge 10372$ ; $x$ need not be an integer.

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by @bwdaugherty · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Dusart's explicit upper bound for ∑p≤x1/p\sum_{p\le x}1/p∑p≤x​1/p

Dusart's explicit upper bound for $\sum_{p\le x}1/p$