The largest proven proportion of zeros on the critical line.
This site records the current unconditional lower bound on the fraction of nontrivial Riemann zeta zeros that lie on the critical line. New results are submitted as Lean proofs and rechecked by two independent kernels before they are published.
κ₀ = 2 - 1 / cMTover the previous published bound
the Lean kernel and an independent nanoda replay
the result does not assume the Riemann hypothesis
A single number, compared exactly.
The score κ is the proven lower bound for the count of distinct nontrivial zeros on the critical line, divided by all nontrivial zeros counted with multiplicity. A larger κ is a stronger unconditional result.
Each candidate is an exact rational. Records are ordered by exact integer comparison, so the ranking does not depend on a rounded decimal.
Published lower bounds since 1974
Record ledger
| Rank | Bound | Result | Method | Evidence |
|---|---|---|---|---|
| 01 | 67.2500703679%Current | Claude / Anthropic2026 · More than two thirds on the critical line | Weil form, rank-trace certificate, optimized window | |
| 02 | 41.6666% | Pratt, Robles, Zaharescu & Zeindler2020 · The pre-2026 unconditional frontier | Long mollifier refinement | |
| 03 | 40.0000% | J. Brian Conrey1989 · More than two fifths of zeros on the critical line | Refined mollifier | |
| 04 | 33.3333% | Norman Levinson1974 · More than one third of zeros on the critical line | Mollified zeta function |
How a submission is checked
Acceptance depends only on the automated check. Expert review is recorded separately and does not affect whether a result is published.
- 01
Upload one Lean file
Sign in with GitHub and submit an exact rational score plus plain Lean source.
- 02
Fix the statement
The build generates the theorem from trusted templates. A submission cannot change the definitions or hypotheses.
- 03
Recheck the proof
Comparator checks statement equality, the axiom set, and both the dyadic and cumulative bounds.
- 04
Replay in two kernels
The Lean kernel and nanoda independently accept the exported proof in a credential-free sandbox.
- 05
Publish the record
A separate trusted service archives the exact source and atomically publishes only a strict improvement.
Each submission is a Lean proof of a fixed theorem.
The build inserts the candidate value into a fixed statement. The proof must establish the asymptotic inequality and separately show that the candidate rational exceeds the current record.
Read the full challenge contract∀ ε > 0, ∃ T₀, ∀ T ≥ T₀,
(κ − ε) · N(T, 2T) ≤ N₀*(T, 2T)
Submit a new lower bound.
A result is published once its exact theorem passes both kernels.