More than 83.69% of the zeros of the Riemann zeta function are distinct
Kristian Muri Knausgård
math.NT
Sep 27, 2026 · v1
cs.AI cs.LO
TL;DR
Key matrix inequalities, threshold lemma, block dichotomy, counting assembly and exact arithmetic for the zeta zero bound are formalized in Lean 4 with Mathlib.
Abstract
The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, counted with multiplicity, is at least $0.8369928814\ldots$. The previous bound was $0.83625\ldots$. As in the proof of that bound, an unconditional version of Montgomery's pair-correlation theorem gives an asymptotic energy estimate. The new ingredient is a short matrix inequality with a free clipping parameter. It strengthens the lower bound for this energy in terms of the number of distinct zeros. The gain is a nonnegative correction from overlaps between different nearby zeros on the critical line, which is retained even when some of these zeros are double. The matrix inequality, the threshold lemma, the block dichotomy, the counting assembly and the exact arithmetic are proved formally in Lean 4. The constant relies on a computer-assisted local inequality from recent work that has not yet been refereed. That computation was re-run independently, and every imported input is listed. This paper is primarily an experiment in AI-assisted mathematical research (Section 4).
Problem
Bounding the asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, counted with multiplicity, improving the previous lower bound of 0.83625.
Approach
An unconditional version of Montgomery's pair-correlation theorem gives an asymptotic energy estimate. A new short matrix (Gram) inequality with a free clipping parameter strengthens the lower bound on this energy in terms of the number of distinct zeros. The matrix inequality, threshold lemma, block dichotomy, counting assembly and exact arithmetic are proved formally in Lean 4 with Mathlib, with unformalized analytic inputs entering as explicit hypotheses. A computer-assisted local inequality certificate was re-run independently.
Results
The lower asymptotic proportion of distinct nontrivial zeros is at least 0.8369928814..., improving the previous 0.83625... bound. The Lean proofs contain no sorry and depend only on propext, Classical.choice and Quot.sound.
