Analytic number theory·zeta:critical-line-proportion
Proportion of zeta zeros proved to lie on the critical line
Machine-checked by qed.bot.
Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
The Riemann hypothesis asserts that every nontrivial zero of the zeta function lies on the critical line. Short of proving it, mathematicians bound the proportion of zeros that provably do.
Record history
5 steps·proportion of zeros, higher is betterSelberg proved in 1942 that a positive proportion of the zeros lie on the line, without an explicit constant. Levinson's method gave more than a third in 1974, and refinements of it carried the bound past two fifths and, by 2018, to just over five twelfths. The 2026 step proves a stronger statement, that the zeros are simple as well as on the line; its paper says the proof was discovered by Claude and verified and communicated by Levent Alpöge and Ralph Furman.
At least two thirds of the zeros, counted with multiplicity, are simple and on the line, and 0.6725 with the Montgomery–Taylor window; at least five sixths are distinct. Announced on 10 August; the paper, with its Lean formalisation, followed on arXiv on 13 August.
Slightly over five twelfths; published in Research in the Mathematical Sciences in 2020.
Published in Acta Arithmetica in 2011.
More than two fifths of the zeros lie on the critical line.
More than one third of the zeros lie on the critical line.
AI activity
How grades workProved that at least two thirds of the zeta zeros are simple and on the critical line, 67.25% with a refined window, raising the proven proportion on the line from just over five twelfths; at least five sixths are distinct.
Reasoning and sources
Autonomy
The prompt was to attempt the Riemann hypothesis; the mathematical choices were the model's, the paper states the proof was discovered autonomously by Claude, and the accompanying formalization.yaml records the work as autonomous. Humans validated the result rather than contributing to it.
Autonomy declared autonomous in the project's formalization.yaml.
Details
method: Two Claude Code sessions, 31 million output tokens, roughly 60 subagents
review: Examined by Brian Conrey and Dan Goldston; formalisation author-verified by Ralph Furman
Fidelity
How fidelity is gradedF2 declared. The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Checks
1-
verified·qed.bot
23 theorems on the standard axioms only, at cec57f91
Declared by the projects
1As each project's formalization.yaml states it.
Zeta23 — more than two thirds of the zeta zeros are simple and on the critical line
- authors
- Claude
- method
- autonomous — Claude
- review
- author-verified (Ralph Furman)
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 5 main results named, checked with Comparator, with an alignment table
- sources
- More than two thirds of the zeta zeros are simple and on the critical line — formalizes, authors participated
- related
- AlexKontorovich/PrimeNumberTheoremAnd — adapts
- divergences
- liminf bounds are rendered as: for all ε > 0 there is T₀ such that for all T ≥ T₀, (c − ε)·N ≤ X. "Nontrivial zero" is rendered as a zero with 0 < Re ρ < 1. Windows are T₁ < Im ρ ≤ T₂ (positive ordinates). Left sides count with multiplicity; N₀*, N₀ˢ, N_d count distinct points (the strong direction). Theorem B of the paper is formalized for primitive characters of modulus q > 1. The repository states the theorems at the paper's constants; the weaker Cauchy–Schwarz-form variants that earlier revisions also certified are implied by these and are no longer separately stated. The 5/6 constant is obtained from the rank–trace inequality with parameter c = 3 where the paper's text uses Proposition 4.5(iii) with c = 2. (In the non-submitted ξ′ configuration the proportion statements carry fixed decimal constants rather than ε-forms.) See README.md, "Reading notes for the statements".
- checked by
- qed.bot
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themRecorded elsewhere
Compare the registries- vibemathed — Absence of critical Bernoulli bond percolation on ℤ^d in every dimension d ≥ 2
- vibemathed — The Proportion of Zeta Zeros on the Critical Line
Sources
Cite this record
qed.bot, “Proportion of zeta zeros proved to lie on the critical line”, https://qed.bot/t/zeta-critical-line-proportion, as of 30 Sep 2026.