Papers With

← All papers
First page of More than two thirds of the zeta zeros are simple and on the critical line

More than two thirds of the zeta zeros are simple and on the critical line

Levent Alpöge, Ralph Furman

math.NT Aug 13, 2026 · v1
formalization number-theory
Read PDF arXiv abstract
TL;DR
An unconditional theorem that at least two thirds of zeta zeros are simple and on the critical line is formally verified in Lean 4.
Abstract
We prove unconditionally that at least two thirds of the nontrivial zeros of the Riemann zeta function, counted with multiplicity, are simple and lie on the critical line, and that at least five sixths are distinct; the previous unconditional records are $\frac{5}{12}$ and $0.6603$. With the Montgomery–Taylor window the constants become $0.6725$ and $0.8362$. The argument makes Montgomery's 1973 deduction unconditional: the Riemann hypothesis, classically needed to read the zero side as a positive sum over real ordinates, is replaced by a rank-trace inequality applied to a finite compression of Weil's Hermitian form, with Sylvester's law of inertia handling off-line pairs. The analytic inputs are those of Aryan and of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh. The results extend to primitive Dirichlet $L$-functions and are formally verified in Lean 4.
Problem

Determining unconditional lower bounds on the proportion of nontrivial zeros of the Riemann zeta function that are simple and lie on the critical line, and the proportion of distinct zeros. Previous unconditional records were 5/12 for simple on-line zeros and 0.6603 for distinct zeros.

Approach

Montgomery's 1973 conditional deduction is made unconditional by replacing the Riemann hypothesis with a rank-trace inequality applied to a finite compression of Weil's Hermitian form, using Sylvester's law of inertia to handle off-line zero pairs. The explicit formula and a test-function family are combined with linear-algebraic lemmas (inertia under pull-back, rank-trace inequality, Weyl bounds). Analytic inputs from Aryan and Baluyot-Goldston-Suriajaya-Turnage-Butterbaugh supply the Frobenius norm estimate. The main results are formally verified in Lean 4.

Results

At least two thirds of nontrivial zeta zeros (with multiplicity) are simple and on the critical line, and at least five sixths are distinct. With the Montgomery-Taylor window the constants improve to 0.6725 and 0.8362. Results extend to primitive Dirichlet L-functions.