The Proportion of Zeta Zeros on the Critical Line
Statement
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 had crept to about 41.6%. This proves at least of zeros are simple and on the line, and that at least 0.83625 of zeros are distinct.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
Claude (unreleased research version), with Jarred Sumner, Levent Alpöge, Ralph Furman and Eric EasleyThe record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.
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.
Machine-checked by Lean on #1 · not a person
lean: partially checkedLeanscope Lean formalization of the core argument; statement correspondence not independently audited
A sorry-free Lean 4 / Mathlib formalization accompanies the paper, and the headline statements are built from Mathlib's own riemannZeta and analyticOrderAt with the corresponding counting functions, rather than from an assumed form of the result. Curator check: the repository is real and substantial, 329 Lean files, Apache licensed to Anthropic.
Held at the unaudited rung rather than promoted, for a specific reason. Building on Mathlib primitives is real statement anchoring and reduces drift, but the assembly of those primitives into the proportion claim is the paper's own, and that assembly is exactly what nobody independent has audited. The same organisation produced the proof and the formalization.
On human review: two Anthropic mathematicians studied and validated the work, and Brian Conrey and Dan Goldston examined the paper on short notice. That is meaningful scrutiny but not the top verification rung, which asks for named experts with no stake who endorse the claim. The announcement reports examination rather than endorsement, and Goldston is an author of the prior work the result builds on.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.