The Proportion of Zeta Zeros on the Critical Line
The Riemann hypothesis asserts that every nontrivial zero of the zeta function lies on the critical line. Short of proving it, the standard measure of progress is the proportion of zeros known unconditionally to lie there: Selberg established a positive proportion, Levinson reached a third in 1974, Conrey two fifths in 1989, and the record stood at for zeros that are simple and on the line, and for distinct zeros.
Under the Riemann hypothesis, Montgomery deduced simple from the pair-correlation second moment in 1973. His prime-side evaluation was already unconditional; RH entered only to read the zero side as a positive sum over real ordinates. Goldston and Suriajaya isolated that termwise positivity as the remaining obstacle and asked what would follow if it could be removed.
This removes it, proving unconditionally that at least of zeros are simple and on the line and at least are distinct - and with the Montgomery-Taylor window.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Analytic number theory
- Posed by
- Bernhard Riemann (1859) for the hypothesis; the proportion ladder runs from Hardy and Selberg through Levinson and Conrey
- Year posed
- —
- Years open
- —
- Solved
- 2026-08-10
- Model
- Claude (unreleased research version)
- Vendor
- Anthropic
- Collaborators
- Jarred Sumner, Levent Alpöge, Ralph Furman, Eric Easley
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 68 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
An unconditional record, not a resolution: the Riemann hypothesis is untouched, and Anthropic states it does not expect these techniques to lead to a proof of it. The paper is explicit that these are lower bounds only - the remaining third of the zeros are not shown to be off the line, merely not reached by the certificate.
What it does settle is a question that was posed. Goldston and Suriajaya had reduced Montgomery's conditional to a single obstruction, the termwise positivity that fails for zeros off the line, and asked what would follow without it. Theorem A replaces that positivity with a rank-trace inequality on a finite compression of Weil's Hermitian form, with Sylvester's law of inertia handling off-line pairs; reading the negative index of truncations as a count of off-line pairs is Bombieri's device. The paper also proves the bound sharp for this route: improving on this way would need pair-correlation information beyond Fourier support 1.
What the AI did
Claude was asked to take a real stab at the Riemann hypothesis, with the mathematical choices left to it, and the bound improvement came out as a byproduct of failing at that. It generated and discarded roughly 650 ideas in a first session; in a second it coordinated about 60 subagents which ran some 2,400 shell commands, wrote hundreds of scripts, checked numerically against known zeros and refereed one another. Two subagents developed the key ideas, thirteen fed them, thirty tried and failed, thirteen validated, two drafted the paper. Roughly 31 million output tokens across two Claude Code sessions.
The decisive step was combining the unconditional pair-correlation work of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh with a 2000 paper of Bombieri, treating the whole function space at once with the quadratic form allowed to be non-diagonal rather than splitting it. Claude also proposed writing the result up, checked 54 arXiv papers for prior art, and recommended that a human number theorist validate it.
Verification
A sorry-free Lean 4 / Mathlib formalization accompanies the paper, with the statements built from Mathlib's own riemannZeta and analyticOrderAt rather than an assumed form of the result. This site audited the sources at tag v1.0: no sorry under Zeta23/, the 27 real ones all in the comparator/Challenge files that state the theorems with placeholder proofs by design; no native_decide; no axiom declarations - the two a plain grep reports sit inside a tactic's docstring.
One finding changes the entry's meaning: the headline theorems are unconditional, not modulo literature inputs. Zeta23.thmA0 takes no hypotheses, because Weil's explicit formula is itself proved in Lean from Mathlib's functional equation, as are Riemann-von Mangoldt, Montgomery-Vaughan, Stirling and Chebyshev-Mertens.
Still held at the unaudited rung, for the reason that tier exists: the trusted statement files are written in the same repository by the same team, so nobody independent has checked the Lean statement against the paper's claim. The repository ships a leanprover/comparator challenge-and-solution split built for exactly that audit - running it is what a promotion would take. The kernel was not re-run here; the axiom lines are the repository's own record.
On human review: two Anthropic mathematicians validated the work, and Brian Conrey and Dan Goldston examined the paper. Examination is not endorsement, and Goldston is an author of the prior work this builds on.
Sources
- PaperMore than two thirds of the zeros of the Riemann zeta function are simple and on the critical lineThe Anthropic PDF the entry was first written from, before the arXiv versionAnthropic's informal note stating the proof concisely
- Lean proofLean repository - audited at tag v1.0; comparator statements under comparator/
- TranscriptAnnotated subagent transcripts
- AnnouncementAnthropic's announcement
- OtherHow the argument was found: Claude's account of its own two runs
FrontierStep on Zeros on the critical line · · current best
Submitted by SwiftTapir695 on
For the "open number of years" case, I think partial results can fairly claim the years since the previous best result was known. Wikipedia says, "In 2020, the [RH percentage of zeros on the critical line] estimate was extended to five-twelfths (i.e., 41.6%) by Pratt, Robles, Zaharescu and Zeindler[43]", so it should be justifiable to say this is an improvement on a six-year problem.