On the proportions of simple and of distinct zeros of the Riemann zeta function

Abstract

We prove, without hypotheses on the zeros and with computer-assisted steps, that, as T → ∞, at least 0.676102666 of the zeros ρ of ζ(s) with T < Im ρ ≤ 2T, counted with multiplicity, are simple, and at least 0.838051333 of them are distinct. The largest previous unconditional bounds that we located in the refereed and arXiv literature are, truncated, 0.67250077 for simple zeros, which is the bound for simple zeros on the critical line, and 0.83625038 for distinct zeros. Unrefereed computer-assisted claims for simple zeros on the line at bandwidth one reach 0.67349239; the three largest of them use the fixed-test-function pair-correlation formula, as Lamzouri does, rather than the inputs of Alpöge and Furman used here. Two unrefereed works claim considerably more by other means, and we have not verified them. The argument extends the rank–trace method of Alpöge and Furman. With a smaller computer-certified local inequality (K = 5 consecutive zeros instead of 7) it gives the slightly smaller pair 0.675158622 and 0.837579311. For this pair the whole proof, the local certificate included, is checked by the kernel of Lean 4 with no hypotheses. For the K = 7 pair and for the two statistics below, everything except the local certificate (the analytic and algebraic steps, the majorant certificate and the closing arithmetic) is checked by the kernel, and the local certificate enters as a single displayed hypothesis, verified outside Lean by interval arithmetic. Two further statistics are recorded. At least 0.6733736895 of the zeros are simple and on the critical line, by a method that others published first; this is not a record, since for this statistic six unrefereed works announce larger values, from 0.673399 to 0.67349239, one of them (0.6734) as a hypothesis-free Lean theorem, whereas our formal statement carries a certificate hypothesis. At least 0.8879195 of the zeros are simple or on the line, which is Lamzouri's formula evaluated at 0.6733736895. The results are lower bounds only and say nothing about the Riemann hypothesis itself.

Keywords