How many zeta zeros are simple and sit on the critical line? Two answers are proved outright. Anthropic's is 67.25007%. zeta-lab's is 67.28470%, built on theirs, with the certificate proved in Lean instead of assumed.
There are bigger numbers out there, two of them zeta-lab's. All of them assume a certificate nobody has proved yet, so they are claims rather than theorems. Below is what was run and what came back, the dead ends too. Every figure links to the run behind it.
Everything else on this site is self-asserted, however carefully. Two results are not. Each was submitted to the Palomar Registry, which fetched a pinned commit, rebuilt the development on its own hardware inside a sandbox, and replayed the proofs through Lean's kernel and through a second kernel written independently of it.
The n-point simple-zero bound (PALOMAR-2026-08-25-000005), registered 25 August 2026: the parametric theorem and four instances, of which the three- and four-point ones are unconditional, their certificates proved in Lean rather than assumed. This is where the 67.28470% above comes from. The eight-point instance keeps its certificate as a named hypothesis and is listed as conditional.
The source-admissible strong closure (PALOMAR-2026-08-21-000004): a statement about a Fredholm operator on an interval and about a class of test profiles.
The analytic half of Davenport-Heilbronn (PALOMAR-2026-08-21-000012), which the registry classifies source-based, meaning it formalizes an existing theorem rather than establishing a new one. Davenport and Heilbronn are cited for zeros off the critical line, and that half was not proved here.
None of them says anything about the Riemann hypothesis, and none is peer review: no person read any of them. What the registry did is mechanical, and it is described in full below.
| who | fraction | status |
|---|---|---|
| Furman and Alpöge, Anthropic | 67.25007% | proved, Lean-checked end to end at zeta-23-lean |
| here | 67.28470% | proved, built on the above; the four-point certificate proved in Lean, standard axioms only |
| here | 67.27373% | proved, the three-point instance, same standard |
Same three steps every time: reproduce the certificate from the author's own artifacts, read the step that accepts it, then measure how far that parameterisation can go.
Interval-arithmetic certificates for the proportion of simple zeta zeros on the critical line . The verifier pruned on a threshold derived for the original target and never re-derived when the target was raised, so raised-target runs reported a check they had not performed. Repaired and reported upstream; every published result survives it.
Record: hunts/ainta_seven_point
Wikstrom's computer-assisted lower bound for Bloch's constant (arXiv 2608.17660) . His own verifier, unmodified, on his own certificate data, accepts 0.0153040536 against a published 0.0153: all 24 away sectors, all 38,400 cells, none refused. The certificate supports more than the paper claims for it, and the paper's own bound stands unchanged.
Record: hunts/bloch_ceiling
An exact-pressure certificate for the same proportion, published with its whole pipeline . At its author's own pinned tip the pipeline returns INCONCLUSIVE, 1.19e-07 short of target, while all six interval tables reproduce byte for byte. Fail-closed: not evidence the bound is wrong, only that it does not re-verify from a fresh clone. A 70-line reproducer isolates it.
Record: hunts/amtopa_ceiling
The Delsarte linear-programming bound for kissing numbers . The node-discretised step is a relaxation, so its optimum sits below the truth: 196505.76 in dimension 24 where the answer is 196560. Sweeping degree 1 to 30, the value stops moving by degree 14, so the headroom is in the node set, which nobody publishes.
Record: hunts/r_6f0f63
Erdos's minimum overlap constant . The piecewise minimax stalls 1.6e-4 above Haugland's published value, and the stall is provably the solver's rather than the family's. This hunt's own best exact bound is weaker than the published one, and is recorded as weaker.
Record: hunts/r_828c8b
The Riemann hypothesis says every one of infinitely many special points sits exactly on a particular line. Proving that outright is the open problem, and nothing here touches it. Proving that at least some fraction of them do is the ground people actually gain, and that fraction has been the scoreboard for a century.
Two days after Anthropic's paper this laboratory assembled and audited a chain that would carry 67.25007% to 67.25107%, with one step of that chain still open, and produced 5 theorems of its own along the way, each one checked by the Lean kernel with no sorry, no native_decide and no floating point.
i. The census floor: c_u ≥ 5.021172019×10⁻⁶ for the genuine MT kernel (Real.sin, Real.sqrt 2, π, not a rational surrogate), by explicit rational weak duality plus four kernel bounds proved with from-scratch Taylor machinery and explicit truncation error. Stated for any cost vector dominating those four bounds, so it survives their re-derivation.
Kernel-checked in FloorCert.lean · read the specification
ii. The retention certificate's arithmetic: the recorded band-dual cover closes at its four depths, with cap defined by the genuine band supremum and infimum of ω², so the recorded numbers enter only as one-sided bounds and the statement cannot be vacuous, together with "no band was missed" as a property of the cover.
Kernel-checked in BandCert · read the specification
iii. The composition inequality s ≥ 2N − ‖P+Q‖²_F + D, with the corollary that ‖P+Q‖²_F ≤ C·N and D ≥ θ·R₀ give s ≥ (2−C)N + θR₀. This is what removes the question "does θ really enter multiplicatively?": it is exact arithmetic, not analogy.
Kernel-checked in t3_composition_skeleton.lean · read the specification
iv. The grid-incidence law Σ_{n∈ℤ} φ̂(x−n)φ̂(y−n) = 2π·FT(φ²)(x−y) for even, bounded, measurable φ supported in [−½, ½]. Continuity is not assumed, which matters: the paper's window jumps at the box edge.
Kernel-checked in law_d_incidence.lean · read the specification
v. The Pub 1 source-admissible strong closure: the supremum of ⟨1,v⟩²/⟨Av,v⟩ over the source-admissible class is c* = ⟨1, A⁻¹1⟩, with the reciprocal orientation as the matching infimum, and orientation_not_symmetric recording that the two quotients are genuinely different quantities so the load-bearing orientation cannot be silently swapped. Unconditional since 2026-08-16 (this row read Conditional until then; see below). The four analytic facts about w that were carried as explicit named hypotheses have all been discharged, strongClosureData_final holds with no analytic or membership hypothesis, so pub1_strong_closure assumes only IsProfile w, which is the setting rather than a hypothesis about it, and pub1_strong_closure_exists carries no hypothesis at all, so nothing is vacuous. The tree is sorry-free and axiom-clean (propext, Classical.choice, Quot.sound) against pinned Mathlib v4.33.0-rc2.
Kernel-checked in Pub1.lean, status in OBLIGATIONS.md · read the specification
Fractions of a percent are how this problem moves. Each one has taken the field years, argued on paper until this month. Anthropic's step is Lean-checked, and so is the floor under this one, against the real function rather than a rational surrogate for it.
A composite claim takes the grade of its weakest step, and nothing here is rounded upward. 2,235 automatic checks run under the first two rungs.
sorrys, standard axioms only. These are theorems and are called theorems.Every tool in this table is available to anyone, so it is worth naming which parts carried the weight.
| tool | version | what it did |
|---|---|---|
| Lean 4 + Mathlib | v4.33.0-rc2 | the proof kernel. Nothing counts until it accepts. |
| Aristotle | Harmonic | proof search. Statements are specified here, proofs are machine-found, and the kernel checks them. It also refuted one of our own statements. |
| Arb, via python-flint | 0.6 | ball arithmetic. Carries an enclosure through every step. |
| mpmath | 1.3 | arbitrary precision, the second interval backend, and the independent oracle the suite checks itself against. |
| PARI/GP, via cypari2 | 2.2 | a third oracle, written by a different community over forty years with different algorithms and no shared code. Agreement with mpmath is evidence about the mathematics rather than about one library. |
| Modal | 14 scripts | the compute the certificates were verified on. Shards a search across containers, which is what made an eight-point certificate affordable at a couple of dollars. |
| Inspect | 0.3.250 | the eval runner, from the UK AI Security Institute. Runs the evaluation this laboratory makes of itself, scored by a checker rather than by a judge. |
| numpy | 2.0 | bulk statistics |
| scipy | 1.14 | quadrature and interpolation |
| sympy | 1.13 | exact symbolic work |
| matplotlib | 3.9 | figures |
| pytest, with xdist | 8.0 | the suite. 183 test files, run in parallel; the first two rungs of the ladder are what it checks. |
| Antigravity | agent CLI | sessions across the tree. |
| Claude Code | agent CLI | sessions across the tree, captured in telemetry. |
| Codex | agent CLI | the higher-xi / RAMS2 / RC2 formalization relay. Three modules landed kernel-checked after audit by six independent auditors; nothing was landed on trust. |
The working paper, the obligation ledger, every hunt, every frozen protocol and every correction, in full rather than summarised.
572 documents, 138,654 lines, indexed straight off the tracked file list, and each one a page on this site. The laboratory's housekeeping is not among them: the instructions its workers read, the handoffs, the harness's notes on itself. Those stay in the repository, which is public. The library →
The most recent work in the tree, on any branch, merged or not, newest first and read off git. Upkeep is not listed: the site, the harness, the scripts, the instructions this laboratory keeps for itself.
| when | what | commit |
|---|---|---|
| 2026-09-28 | Sanitize three machine-local paths in the published four-point… | 958877c |
| 2026-09-28 | Publish kernel-build evidence for the c=2330/10^6 four-point… | 5723f19 |
| 2026-09-28 | Pass independent L119 bound and preserve complete referee… | 6f7d665 |
| 2026-09-28 | Reconcile all recovered blocks before final L119 reduction | 5324881 |
| 2026-09-28 | Reconcile preemption and recover only nine interrupted L119… | 119280a |
| 2026-09-28 | Check CC polynomial moments and pole normalization in the… | b47690b |
| 2026-09-28 | Checkpoint the L119 bound before the negative control | 58e95b8 |
| 2026-09-28 | Make exact triangular factor semantics explicit in referee… | e5f8885 |
Branches carrying commits that are not on main, read off git.
| branch | what | last |
|---|---|---|
| teal-sea/weil-c4-s2 | hunts(weil_propagation/c4_s2): RESULTS line 1, scope of the… | 2026-09-24 |
| claude/weil-c4-s2-cloud-sweep-tobmhh | hunts(weil_propagation/c4_s2): cloud sweep: review fixes… | 2026-09-24 |
| teal-sea/weil-c4-s2-cloud | hunts(weil_propagation/c4_s2): cloud sweep: review fixes… | 2026-09-24 |
| claude/phase3-ts-checker-sweep-um4ud5 | hunts(weil_propagation/c4_s2/checker): phase 3 T_S sweep re-run… | 2026-09-24 |
| teal-sea/weil-propagation-theory | hunts(weil_propagation/theory): fix scope of the 8449c29… | 2026-09-23 |
| teal-sea/weil-propagation | hunts(weil_propagation/numerics): CI proposal for… | 2026-09-23 |