More than 83.69% of the zeros of the Riemann zeta function are distinct
Kristian Muri Knausgård
math.NT
Sep 27, 2026 · v2
cs.AI cs.LO
TL;DR
The matrix inequality, threshold lemma, block dichotomy, counting assembly and exact constants are formalized in Lean 4 with Mathlib; the code contains no sorry.
Abstract
The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, relative to the total number counted with multiplicity, is at least $0.8369928814\ldots$. Earlier work proves $0.83625\ldots$, and a report we have not verified claims $0.83672\ldots$. As in the proof of the bound $0.83625$, 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
Bound from below the asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, relative to all zeros counted with multiplicity. The best earlier unconditional bound was 0.83625.
Approach
Zeros are encoded as wave-packet vectors that form a Hermitian operator. An unconditional form of Montgomery's pair-correlation theorem gives the asymptotic energy tr A^2. A new mixed-multiplicity Gram matrix inequality with a free clipping parameter strengthens the energy lower bound by retaining overlap corrections between nearby zeros. The matrix inequalities, block dichotomy, counting assembly and arithmetic are proved in Lean 4. The analytic inputs and a computer-assisted local inequality enter the Lean statements only as explicit hypotheses.
Results
The liminf of N_d(T)/N(T) is at least 0.83699288145. The Lean proofs use only the standard axioms (propext, Classical.choice, Quot.sound). The imported Arb-based certificate was re-run independently, and the work was developed with substantial AI assistance.
