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 Anthropic 2026 starting record
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.
Riemann.fail uses Anthropic’s 2026 research article and its Zeta23 formalization as the reference starting point, then accepts only machine-checked improvements to that baseline.
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 |
Submit from the site, or run the verifier yourself.
Sign in and upload a Lean proof, or clone the repository and check it locally. A coding agent can drive the whole loop.
From the site
Sign in with GitHub, then paste an exact bound and its Lean proof. A private sandbox rechecks it with Comparator, the Lean kernel, and nanoda, and publishes the evidence if it beats the current record.
Submit a resultLocally, or with a coding agent
git clone https://github.com/josusanmartin/riemann.git
cd riemann && npm install
# add submissions/<name>/submission.json + proof/Solution.lean
npx tsx scripts/verify-submission.ts submissions/<name> --mode=quick
# then upload proof/Solution.lean at https://www.riemannzeta.fun/submitPoint a coding agent at the repository and its CONTRIBUTING.md to run clone → improve → verify. Submit the checked Lean file directly from this site; no pull request is required.
How a submission is checked
A durable FIFO runs one proof at a time, with three uploads per GitHub account each UTC day. Acceptance depends only on the automated check; expert review is recorded separately.
- 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.