Anthropic reports a new Riemann-zeta lower bound, with a public Lean audit target

Anthropic says an unreleased research version of Claude raised the known lower bound for the proportion of nontrivial zeros of the Riemann zeta function on the critical line from 41.6% to 67.2%. The research page was published on 10 August 2026 at 17:00 UTC. Alongside the claim, Anthropic released a paper, an informal note, and a public Lean formalization repository, zeta-23-lean.

A published claim with a public Lean target

The useful part of this announcement is the inspectable artifact. The repository README records a sorry-free formalization, Lean v4.33.0-rc2, and a pinned Mathlib commit. Those details give an outside reader something more concrete than a model demo or a result described only in prose. They also make the environment part of the claim: a replay should record the repository commit, compiler, library revision, and build output.

The number is not the hypothesis

A lower bound of 67.2% does not show that all nontrivial zeros lie on the critical line. It is not a solution of the Riemann hypothesis, and a successful repository build would not by itself prove that the paper has been interpreted correctly. The theorem, its assumptions, its correspondence with the paper and informal note, and the meaning of the reported bound still have to be examined together.

An audit path for the repository

1. Clone the public repository and save the exact revision.
2. Use the Lean and Mathlib versions recorded in the README.
3. Run lake build, the project comparator, and #print axioms as documented.
4. Compare the formal theorem and assumptions with the paper and informal note.
5. Record the toolchain, library revision, build result, comparator result, and axiom output.

This can reproduce the repository state and expose its formal dependencies. It cannot establish conclusions that the checked theorem does not represent.

What outside review must settle

Anthropic says its mathematicians reviewed the work and reports that Brian Conrey and Dan Goldston examined it on short notice. Those are descriptions of the company's review, not independent confirmation. The right editorial label remains precise: Anthropic-reported lower bound, public formal artifact, independent mathematical review still pending.

Sources: Anthropic Research: Riemann zeta and zeta-23-lean.