Cumulative Prime Sums and Riemann Zeros: A fine grid, its ripple, and a family of prime races

A mix of human-written and AI-generated textHuman understanding: some partsmath.NT — Number Theorycs.LO — Logic in Computer Sciencemath.PR — Probability

Contributed by Antonio Mennillo ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

Summing the primes one after another and taking logarithms gives an increasing sequence of real numbers, σm=log⁡Spm\sigma_m=\log S_{p_m} with SN=1+∑p≤NpS_N = 1+\sum_{p\le N}p, which becomes exponentially dense. The ordinates γn\gamma_n of the zeros of the Riemann zeta function fall on this grid with tiny errors: 1.4⋅10−31.4\cdot10^{-3} at the first zero, 2.4⋅10−72.4\cdot10^{-7} at the fifth, 3⋅10−173\cdot10^{-17} at the twentieth. Part I explains why. The cell of the grid containing a height tt has width (1+o(1))t e−t/2(1+o(1))\sqrt t\,e^{-t/2} (Step Theorem), and every real t>log⁡3t>\log 3 has a node above it within that width, by an argument going back to Bertrand's postulate (Covering Theorem). The precision observed at the zeros is therefore the resolution of the grid, and the same precision holds at every height (Genericity Principle). We compute the first-crossing primes NnN_n with certification up to n=20n=20 and test, in a protocol fixed before the computation, whether the zeros sit closer to the nodes than a generic height. Neither the mean distance to the nearest node (0.2460.246 against 0.2500.250, p=0.92p=0.92) nor the distribution of the position within the cell (Kolmogorov–Smirnov, p=0.79p=0.79) departs detectably from the generic case, and an integer grid used as control behaves in the same way. We also correct the half-exponent law by a factor t′/t\sqrt{t'/t}. Part II shows where the zeros are actually visible. They are not in the position of the nodes but in the ripple: the deviation of the grid from its mean curve B(x)=1+li(x2)−li(4)B(x)=1+\mathrm{li}(x^2)-\mathrm{li}(4). This ripple is a sum of pure oscillations, one per zero; its spectrum shows a peak at each of the first 13 ordinates, with the amplitude predicted by the explicit formula. Under RH the ripple has size e−t/4e^{-t/4} on the grid, much larger than the cell e−t/2e^{-t/2}, and RH is equivalent to this decay rate. The ripple is not centred: on [103,108][10^3,10^8] the sum of the primes stays below li(x2)\mathrm{li}(x^2) for about 97% of logarithmic time, and it first exceeds it at x=109x=109. We place this in a one-parameter family of prime races, ∑p≤xpa\sum_{p\le x}p^a against li(xa+1)\mathrm{li}(x^{a+1}), and prove that under RH the normalized error has mean −1/(2a+1)-1/(2a+1), coming from the squares of the primes. Under RH and LI the limiting logarithmic density of the set where the race is ahead is given by a Rubinstein–Sarnak formula; it moves from 2.6⋅10−72.6\cdot10^{-7} (counting the primes, a=0a=0) to 0.060.06 (summing them, a=1a=1) and tends to 1/21/2 as a→∞a\to\infty, at the rate 12−δa∼1/(2πAlog⁡(A/2π))\tfrac12-\delta_a\sim1/\bigl(2\sqrt{\pi A\log(A/2\pi)}\bigr) with A=a+12A=a+\tfrac12. At a=−1/2a=-1/2 the bias becomes the 12log⁡log⁡x\tfrac12\log\log x of the weighted counting functions of Aoki and Koyama. All theorems are formalized in Lean 4, with the classical results they use as explicit hypotheses.

Provenance statement

AI tools assisted with the numerical computations, the certification pipeline and parts of the drafting, and wrote most of the Lean code, under the author's direction. The author takes full responsibility for the content. All theorems are formalized in Lean 4 with Mathlib in the public repository github.com/anthem87/cps (AGPL-3.0-or-later; release tag cps-v4), with no sorry and only the standard axioms; published classical theorems and one numerical certificate enter as explicit hypotheses. The formalization passes the automated checks of the Palomar registry; its review there is pending. The paper is archived on Zenodo: version 4, doi:10.5281/zenodo.23962478 (all versions: doi:10.5281/zenodo.18142838).

Tools used

Lean FRO
Lean 4 (proof assistant)Version v4.36.0-rc2
Mathlib community
Mathlib (proof assistant library)
FLINT
Arb / python-flint (certified computation)
mpmath
mpmath (numerical computation)
K. Walisch
primesum (prime summation)
AI tools
AI assistant (language model)

References

No bibliography entries.

Version history

  1. v1 · 29 pagesSubmitted by Antonio MennilloInitial depositSupersededNov 05, 2026
  2. v2 · 29 pagesSubmitted by Antonio MennilloSubmitted as a new versionCurrentNov 06, 2026