Claude's 67.2% Riemann Zeta Result: What Was Proved and Verified

Claude did not solve the Riemann hypothesis. It produced a major but precisely bounded result: an unreleased research model found an unconditional proof that at least two thirds of the nontrivial zeros of the Riemann zeta function lie on the critical line, with an optimized constant of about 67.25%. The previous unconditional record was slightly above five twelfths, about 41.67%.

The number is striking. The verification architecture is more important. Anthropic released a full paper, a five-page expert note, a Lean 4 formalization, an audit record, and detailed provenance for the discovery process. Together they form a layered evidence stack in which each artifact catches a different class of failure.

That stack is also the right way to read the claim. A formal proof can check the theorem encoded in Lean. Expert review can check whether the encoded theorem matches the intended mathematics and whether the result is situated correctly in the literature. Open artifacts let other researchers repeat those checks. No single layer substitutes for the others.

What 67.2% actually means

The paper studies nontrivial zeros (\rho = \beta + i\gamma) of the Riemann zeta function. The Riemann hypothesis says every such zero has real part (\beta = 1/2), the critical line.

The new result is a lower bound on a proportion as the height (T) tends to infinity. Its headline statements include:

• At least two thirds of the zeros, counted as distinct points, lie on the critical line.
• At least two thirds are simple zeros on the critical line.
• At least five sixths are distinct.
• An optimized Montgomery-Taylor test family raises the first two constants to about 0.67250 and the distinct-zero constant to about 0.83625.

These are asymptotic, unconditional lower bounds. They do not identify the remaining third as off-line zeros. The method simply does not certify them. The paper explicitly states that its argument has no bearing on the truth or falsity of the full Riemann hypothesis.

This distinction matters for both mathematical accuracy and search intent. The result concerns a proven minimum proportion. It is neither a numerical check of the first 67.2% of zeros nor a 67.2%-complete proof of the hypothesis.

Where the improvement comes from

Earlier unconditional records on zeros on the critical line used descendants of Levinson's mollifier method. The paper cites a 2020 result above (5/12), or 41.66%. A separate line of work began with Montgomery's pair-correlation argument, which could reach a two-thirds constant under the Riemann hypothesis.

Recent work by Baluyot, Goldston, Suriajaya, and Turnage-Butterbaugh made the prime-side pair-correlation evaluation unconditional. The remaining obstacle was the zero side. Without assuming the Riemann hypothesis, zeros can sit away from the critical line, so the relevant quadratic form loses term-by-term positivity.

Claude's paper changes the representation of that obstacle. It restricts Weil's Hermitian form to a finite-dimensional space and reads its structure through linear algebra:

1. A zero on the critical line contributes a positive rank-one form.
2. A symmetric pair of off-line zeros contributes a block with signature ((1,1)).
3. The prime side supplies first- and second-moment information.
4. Sylvester's law of inertia and a rank-trace inequality convert those moments and signatures into a lower bound on on-line zeros.

The novelty lies in combining the indefinite zero-side geometry with the unconditional prime-side information. The argument uses established ingredients, but the bridge between them produces the new bound.

A four-layer verification stack

The safest way to assess an AI-generated mathematical result is to ask what each artifact verifies.

The repository describes a sorry-free formalization under Zeta23/ and Solution, pinned to Lean 4.33.0-rc2 and a specific Mathlib commit. Its audit says the headline theorems depend only on Lean's standard propext, Classical.choice, and Quot.sound axioms. The comparator setup restates the trusted theorem signatures against Mathlib, checks statement equality, and replays proofs in an independent kernel.

Those details close several common loopholes in formal-proof claims. A proof can otherwise compile because a crucial theorem was assumed, because a placeholder remains, or because the implemented statement is weaker than the advertised statement. Axiom inspection and comparator-style statement matching directly target those failure modes.

An independent reviewer can start from the frozen release rather than the moving default branch:

git clone --branch v1.0 https://github.com/anthropics/zeta-23-lean.git
cd zeta-23-lean
lake exe cache get
lake build
lake build Solution Solution.Multiplicity
lake env lean comparator/PrintAxioms.lean
lake env lean comparator/PrintAxioms/Multiplicity.lean

The repository reports thousands of build jobs across the Mathlib dependency closure, so this is a substantial reproduction task. The important property is that its inputs, toolchain, theorem statements, and expected audit output are explicit.

The boundary remains clear. Formal verification establishes that the encoded statements follow from the encoded foundations. Human mathematical judgment is still needed to confirm that definitions, asymptotic quantities, and literature claims express the intended theorem. Anthropic reports that Ralph Furman and Levent Alpöge studied and validated the work, while Brian Conrey and Daniel Goldston examined the manuscript. As of August 11, 2026, the release is one day old, so broad independent scholarly review is still at an early stage.

The discovery process was a search system

Anthropic reports that the model used 31 million output tokens across two Claude Code sessions. The successful session coordinated about 60 subagents, ran about 2,400 shell commands, wrote hundreds of Python scripts, tested candidates against known zeros, searched 54 papers, and asked agents to referee one another.

The important pattern is not the raw token count. It is the separation between exploration and acceptance.

The exploration loop was deliberately high variance. Hundreds of ideas could fail cheaply. Candidate arguments were tested against control objects where analogues of the Riemann hypothesis are false. Agents were asked to name the first unjustified step. The surviving result then moved into a stricter path: re-derivation, expert review, a paper, formalization, statement comparison, and public artifacts.

This resembles a dual-loop protocol for mathematical agents. The outer loop maximizes search breadth. The inner loop minimizes what may enter the trusted knowledge base. The same principle appears in our earlier guide to dual-loop verification for mathematical AI agents.

It also clarifies why a successful AI-generated proof should not be judged by a transcript alone. A transcript documents behavior. A theorem needs a stable statement, a reproducible derivation, and checks whose failure conditions are explicit.

A practical acceptance protocol for AI mathematics

The release suggests a reusable sequence for future AI-assisted discoveries:

1. Freeze the claim. Define the exact theorem, quantifiers, constants, asymptotic regime, and dependencies before promoting the result.
2. Separate discovery evidence from proof evidence. Numerical experiments and failed counterexample searches guide exploration. They do not become premises in the theorem unless explicitly formalized.
3. Run adversarial review. Ask independent agents and domain experts to find the first invalid step, compare against known barriers, and test nearby false objects.
4. Formalize the headline statement. Pin the proof assistant and library versions. Audit placeholders, custom axioms, unsafe declarations, and statement equivalence.
5. Publish the failure surface. State what the method cannot establish, which checks were run, and which parts still rely on expert interpretation.
6. Enable external replay. Release code, source documents, build instructions, hashes, and enough provenance for another team to reproduce the checks.

This is the broader significance of the result. AI can generate enough candidate mathematics that verification becomes the scarce resource. The useful system therefore optimizes for detectable error, not persuasive output.

The same verification ladder also applies beyond mathematics. In Claude's cryptographic discoveries, reproducible attacks and expert validation separated a plausible model output from a security result. In OpenAI's unit-distance problem result, the central question was again how a claim crosses from discovery into accepted knowledge.

FAQ

Did Claude solve the Riemann hypothesis?

No. The hypothesis says all nontrivial zeros lie on the critical line. The new theorem proves an unconditional lower bound of about 67.25%. It leaves the remaining zeros uncertified.

What changed from 41.6% to 67.2%?

The previous unconditional record established that slightly more than five twelfths of the zeros lie on the critical line. The new argument establishes at least two thirds and reaches about 67.25% with an optimized test family.

Does the Lean proof make peer review unnecessary?

Lean checks a formal derivation with very high precision. Expert review checks whether the formal statement matches the intended mathematics, whether definitions and imported results are appropriate, and how the work fits prior literature. The two checks cover different risks.

Can independent researchers reproduce the verification?

The public repository pins its Lean and Mathlib versions, provides build commands, records axiom audits, and includes comparator configurations. Independent reproduction remains valuable because the published audit was produced by the releasing team.

Why is this important for AI-assisted science?

It demonstrates an end-to-end path from broad machine exploration to a narrowly stated, expert-reviewed, machine-checkable artifact. That path is more transferable than any single headline number.

References

• Anthropic: Learning more about Claude's mathematical capabilities
• Claude: More Than Two Thirds of the Zeros of the Riemann Zeta Function Lie on the Critical Line
• Anthropic mathematicians' concise technical note
• Anthropic Zeta23 Lean 4 formalization
• Zeta23 audit record
• Pratt, Robles, Zaharescu, and Zeindler: More than five-twelfths of the zeros of ζ are on the critical line