Analytic number theory·zeta:critical-line-proportion
Proportion of zeta zeros proved simple and 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 that provably do. The constant was raised by hand over several decades to 41.6 per cent.
Record history
Measured in proportion of zeros; maximise.Found while attempting the Riemann hypothesis itself, by combining work of Aryan and of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh with a 2000 paper of Bombieri.
The state of the art before this result, raised incrementally over decades.
AI activity
How grades workRaised the proven proportion from 41.6% to 67.2%, and 5/6 of zeros shown distinct.
Reasoning and sources
Autonomy
The prompt was to attempt the Riemann hypothesis; the mathematical choices were the model's, 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
Does the formal statement say what was claimed?
F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Checks
1-
verified qed.bot
23 theorems on the standard axioms only, at cec57f91
Declared by the projects
1Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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 discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Recorded elsewhere
Compare the registries- vibemathed — Absence of critical Bernoulli bond percolation on $\mathbb Z^d$ in every dimension $d \ge 2$
- vibemathed — The Proportion of Zeta Zeros on the Critical Line