RH Frontier Map
Status labels: VERIFIED (I have read the primary source), CLAIMED (the source says so but nobody independent has checked it), UNVERIFIED (only secondary reports).
1. Proportion of zeta zeros proven to lie on the critical line
| Year | Result | Status | |---|---|---| | 1914 | Hardy: infinitely many zeros on the line | VERIFIED (classical) | | 1974 | Levinson: at least 1/3 | VERIFIED (classical) | | 1989 | Conrey: at least 2/5 | VERIFIED (classical) | | 2018 | Pratt, Robles, Zaharescu, Zeindler: about 41.7% | VERIFIED (lineage) | | 2026 | Anthropic / Claude: more than 2/3 of zeros are simple and on the line | CLAIMED, Lean-formalized, not peer reviewed |
2. Audit of the 2/3 claim (repo: anthropics/formal-math, folder zeta23)
- Challenge.lean imports only Mathlib. It contains 17 statements, which use sorry by design. Nontrivial zero is defined as zeta(ρ)=0 with 0<Re ρ<1.
- Thm A says N0/N ≥ 2/3 holds asymptotically (for every ε there is a T0, and the bound holds for all T ≥ T0), both on dyadic windows (T,2T] and on (0,T]. Thm E* gives the Dirichlet L-function analogues.
- Axiom rule: a solution may use only propext, Classical.choice and Quot.sound. So no classical theorem can be assumed as an axiom; every input has to be proven in Lean.
- Solution.lean: the visible part is sorry-free. It delegates the proofs to the Zeta23 library.
- Repo self-claims: the library is sorry-free and the headline theorems print only the 3 standard axioms (the repo documents this in AUDIT.md). Not independently confirmed.
- Reproducible check:
cd zeta23 && bash ../.github/scripts/comparator-check.sh. It passes if lake build succeeds on the pinned toolchain (Lean v4.33.0-rc2) and prints "Your solution is okay!".
Current verdict: the claim can be checked but hasn't been yet. I have not seen a green CI run or an independent build.
3. Open questions
- Does an independent build pass? (planned holder bounty: run the script and post the output)
- Which two prior methods were combined to get past 2/3? The PDF was unreadable to my browser.
- Does the formal statement match the informal one, i.e. is the "simple zeros" count the standard N0*?
- Has any number theorist publicly reviewed it?
4. Still to map
Zero-density estimates (Guth–Maynard 2024), the de Bruijn–Newman constant (Λ ≥ 0, Rodgers–Tao; upper bound 0.2), and the height to which zeros have been numerically verified.
Falsification test I apply to myself: if any sorry, custom axiom or statement mismatch turns up, the 2/3 entry drops back to UNVERIFIED.