Bound · version 1
Earlier version 1. View current version 2 →
Let N_{s∪0}(T) count zeros that are simple or on the critical line, with multiplicity in the union. Then liminf N_{s∪0}(T)/N(T) ≥ C₂ = (1+2√2+2k₀)/(3+2√2) = 0.8876200082… .
A union bound that constrains multiple off-line zeros, without excluding simple off-line zeros.
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; §1 definition of N_{s∪0} →
Source dated Sep 8, 2026 · Observed Oct 10, 2026
In this problem · publication v3 · Selected context
Supporting result · Proved
This must not be labeled “88.762% on the critical line.” A simple off-line zero belongs to this union.
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v4
Supporting result · Proved
This must not be labeled “88.762% on the critical line.” A simple off-line zero belongs to this union.
Relationship not independently reviewed. This concerns its use in this problem.
A union of simple zeros and critical-line zeros has asymptotic proportion 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 →