More than 83.69% of the zeros of the Riemann zeta function are distinct

Title:More than 83.69% of the zeros of the Riemann zeta function are distinct

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).

Number Theory (math.NT); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

arXiv:2609.33043 [math.NT]

(or arXiv:2609.33043v1 [math.NT] for this version)

https://doi.org/10.48550/arXiv.2609.33043 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

lean/CheckAxioms.lean

lean/MixedGram.lean

lean/MixedGram/Basic.lean

lean/MixedGram/Counting.lean

lean/MixedGram/Threshold.lean

lean/axioms_output.txt

lean/lake-manifest.json

lean/lakefile.toml

replay/README.md

replay/aggregate.json

replay/manifest.json

replay/replay_driver.py

replay/shard-000.json

replay/shard-001.json

replay/shard-002.json

replay/shard-003.json

replay/shard-004.json

replay/shard-005.json

replay/shard-006.json

replay/shard-007.json

replay/shard-008.json

replay/shard-009.json

replay/shard-010.json

replay/shard-011.json

replay/shard-012.json

replay/shard-013.json

replay/shard-014.json

replay/shard-015.json

replay/shard-016.json

replay/shard-017.json

replay/shard-018.json

replay/shard-019.json

replay/shard-020.json

replay/shard-021.json

replay/shard-022.json

replay/shard-023.json

replay/shard-024.json

replay/shard-025.json

replay/shard-026.json

replay/shard-027.json

replay/shard-028.json

replay/shard-029.json

replay/shard-030.json

replay/shard-031.json

replay/shard-032.json

replay/shard-033.json

replay/shard-034.json

replay/shard-035.json

replay/shard-036.json

replay/shard-037.json

replay/shard-038.json

replay/shard-039.json

replay/shard-040.json

replay/shard-041.json

replay/shard-042.json

replay/shard-043.json

replay/shard-044.json

replay/shard-045.json

replay/shard-046.json

replay/shard-047.json

replay/shard-048.json

replay/shard-049.json

replay/shard-050.json

replay/shard-051.json

replay/shard-052.json

replay/shard-053.json

replay/shard-054.json

replay/shard-055.json

replay/shard-056.json

replay/shard-057.json

replay/shard-058.json

replay/shard-059.json

replay/shard-060.json

replay/shard-061.json

replay/shard-062.json

replay/shard-063.json

replay/shard-064.json

replay/shard-065.json

replay/shard-066.json

replay/shard-067.json

replay/shard-068.json

replay/shard-069.json

replay/shard-070.json

replay/shard-071.json

replay/shard-072.json

replay/shard-073.json

replay/shard-074.json

replay/shard-075.json

replay/shard-076.json

replay/shard-077.json

replay/shard-078.json

replay/shard-079.json

replay/shard-080.json

replay/shard-081.json

replay/shard-082.json

replay/shard-083.json

replay/shard-084.json

replay/shard-085.json

replay/shard-086.json

replay/shard-087.json

replay/shard-088.json

replay/shard-089.json

replay/shard-090.json

replay/shard-091.json

replay/shard-092.json

replay/shard-093.json

replay/shard-094.json

replay/shard-095.json

replay/tables.json

(106 additional files not shown) You must enabled JavaScript to view entire file list.

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.