// zeta-23
ZETA-23
A sorry-free Lean 4 formalization of the 2026 two-thirds-of-zeta-zeros theorem.
// in plain terms
In 2026, mathematicians proved that at least two-thirds of the zeros of the Riemann zeta function sit exactly where the Riemann Hypothesis predicts. We rebuilt that entire proof in Lean, a language where a computer verifies every logical step. There are no gaps and nothing that has to be taken on trust.
// 01
Background
The 2026 two-thirds theorem is a landmark on the road to the Riemann Hypothesis. Its proof chains through decades of analytic results that no machine had ever checked end to end: explicit formulas, zero-counting, deep inequalities, all cited on trust.
// 02
Scope of the formalization
PAPER
arXiv 2608.13637
LEAN 4
full analytic chain
MACHINE-CHECKED
8,890 build jobs
0
SORRIES
0
NEW AXIOMS
We formalized theorems A–E and every analytic input they rest on in Lean 4, behind a minimal trusted-statement boundary: Weil's explicit formula for ζ and Dirichlet L-functions, Riemann–von Mangoldt, Stirling, and the Montgomery–Vaughan generalized Hilbert inequality.
// 03
Audit trail
| check | result |
|---|---|
| build jobs | 8,890 — clean |
| sorries in the proof | 0 |
| new axioms | 0 |
| axiom footprint | exactly propext · Classical.choice · Quot.sound |
// 04
Certified results
- +More than 2/3 of zeros are simple and on the critical line; more than 5/6 are distinct. Both are machine-checked.
- +Optimal-window constants: 0.6725 on the line, 0.8363 distinct.
- +A certified ceiling: no bandwidth-one certificate of this kind can exceed 0.6818, the method's own limit, proven.
// the thread
Contribution
None of the mathematics is ours; the theorem belongs to its authors. What we added is a version that does not have to be taken on trust: anyone can replay the build and check it. The one open surface, 256 integer enclosures from external interval arithmetic, is re-derivable from the exact-rational certificate. The work is complete and released as-is.