Bound · version 1
Earlier version 1. View current version 2 →
Let N_s(T) count simple zeros anywhere in the strip and N₀(T) count on-line zeros with multiplicity. Then liminf (N_s(T)+N₀(T))/(2N(T)) ≥ (1+k₀)/2 = 0.8362503518… .
This constrains an average of two different counts.
Proved
Only the exact statement, domain and revision cited by this Claim; this is not a resolution of classical RH or independent OpenMath expert assessment.
Lamzouri · another proof and further proportions · Theorem 1.1: average of N_s and N₀ →
Source dated Sep 8, 2026 · Observed Oct 10, 2026
In this problem · publication v4
Supporting result · Proved
The average does not say that each separate proportion is at least 83.625%. It is a different conclusion from the distinct-zero bound with the same constant.
Relationship not independently reviewed. This concerns its use in this problem.
The average of the simple-zero and critical-line proportions has liminf at least C₁.
paraphrase · No upstream full text or code is republished by this record.
Youness Lamzouri · Preprint
Author preprint at the cited revision; journal acceptance has not been established by this curation.
Source revision: arxiv-v2. Observed Oct 10, 2026.
Lamzouri gives a human-authored proof inspired by the Claude result. Appendix A reports AxiomProver (Axiom Math) autoformalization; this is a different role from discovering the original bound.
Source updated Sep 8, 2026.
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Only the exact statement, domain and revision cited by this Claim; this is not a resolution of classical RH or independent OpenMath expert assessment.
Source dated Sep 8, 2026 · Observed Oct 10, 2026 · Source passage →