On 2026-10-22 this laboratory finished a Lean proof, about Mathlib's own riemannZeta, that every nontrivial zero up to height 50 lies on the critical line and is simple, and that there are exactly ten of them. It is a theorem, in the sense this repository reserves for the word: Lean's kernel accepts it with zero sorry and only the three standard axioms. This page leads with it and carries forward the results of docs/39. On 2026-10-23 a clean Lean source build also closed height 100: 29 distinct zeros in the open critical strip, all on the line and simple. Independent whole-closure replay was accepted by con-ron --verified on 2026-10-24.
The theorems are finite. The height-100 result says nothing above 100 or about the Riemann hypothesis (docs/08). Numerical verification of RH reaches far higher, to 3 * 10^12; the distinction here is a Lean-kernel-checked theorem with no outside computation assumed as an axiom. A bounded search on 2026-10-22 found Lean statements of RH to a height that rest on external computations as axioms, and found no earlier standard-axiom formal proof. That search does not establish priority. The rows carried from docs/39 keep their own grades: they are conditional on OpenAI's theorem and unreviewed by any person.
Every zero rho of Mathlib's riemannZeta with 0 < Re rho < 1 and 0 < Im rho <= 100 has Re rho = 1/2 and analytic order 1; exactly 29 distinct zeros in this window, upper endpoint includedgrade kernel-checked by Lean 4 and Mathlib in a clean source build, zero sorry, three standard axioms only; independent con-ron --verified whole-closure acceptance (earlier bounded attempts inconclusive)
against Numerical RH verification reaches 3 * 10^12 (Platt and Trudgian, 2021). The bounded formal-prior-art search is described in hunt #137; no priority claim
Riemann's hypothesis says every nontrivial zero of zeta has real part 1/2. Computers have checked trillions of zeros, including rigorous interval-arithmetic work, but that is distinct from a formal kernel proof. Hunt #137 first proved height 50 (ten zeros) and then height 100 (29 distinct zeros) in Lean.
Every zero rho of Mathlib's riemannZeta with 0 < Re rho < 1 and 0 < Im rho <= 50 has Re rho = 1/2 and is simple, and there are exactly 10 of them; the same holds to height 52grade kernel-checked by Lean 4 and Mathlib, zero sorry, three standard axioms only; the height-100 final-declaration export has independent whole-closure acceptance, not a separate height-50 export verdict
against RH verified numerically to height 3 * 10^12 (Platt and Trudgian, 2021), a computation, not a formal proof. The closest formal work in the bounded search, gersh/ternary-goldbach-lean, assumes outside computations; anthropics/zeta-23-lean proves a proportion, not individual locations
Lean's kernel and the independent NanoDa kernel accept OpenAI's statements that zeta(s) and every Dirichlet L(s, chi) are nonzero for Re s > 7/8, and its Siegel-zero gap, with only the three standard axiomsgrade kernel-checked on two kernels, on this laboratory's compute; the argument is unreviewed by any person
against OpenAI's own build; no outside replay was known
OpenAI, "The Quasi-Riemann Hypothesis", OpenAI Math Release preprint dated 30 September 2026, Theorem 1.1: every finite-order Hecke L-function over Q(sqrt(-3)), hence every Dirichlet L-function and zeta itself, has no zero in Re s > 7/8. A companion dated 5 October 2026, written with human assistance, proves the weaker half-plane Re s > 11/12 by part of the same method.
h(D) >= sqrt(q) / (10 pi log log q) for every negative fundamental discriminant D, with q = -D; hence the complete list of imaginary quadratic fields of class number h, for every h <= 1500: 9,245,562 fields, the largest with q = 562,394,347grade proved, given the input; constants enclosure-carrying; lists by exact computation; unreviewed
against Watkins (2004): h <= 100 unconditionally. Cremona-Sutherland (2023), section 5: all h <= 1000, including even h, under GRH. OpenAI: the same shape of bound, constant not computed
The class number h(D) of an imaginary quadratic field counts how far unique factorisation fails in its ring of integers. Gauss asked which fields have class number 1; the answer (nine fields) took until Heegner, Baker and Stark, and Watkins completed every h <= 100 in 2004. The difficulty is always the same: a lower bound h(D) >= f(D) that is explicit, so that only finitely many D can have a given class number and one can search them all.
For every integer n >= 1 there is a prime p with n^7 < p < (n+1)^7, given also Kadiri, Lumley and Ng's explicit zero-density estimate; an eighth-power version on the same route is its audited predecessorgrade written conditional candidate, given the input and the density estimate; every numerical step enclosure-carrying; independent written audit by a separate agent context passed; reviewed by no person; not formalized
against k = 9 from the input alone (hunt #126, next row); k = 86 for every n, unconditional (Lee, arXiv:2602.14340, 2026); already known for every n under full RH (Chamberland-Straub)
The October 8 extensions (hunts/oct08_extensions/, PR #282) keep hunt #126's weight, explicit formula and tail routine and add one published input: Kadiri, Lumley and Ng's explicit zero-density estimate (arXiv:2101.12263v1, Lemma 4.14 and Table 1), which bounds how many zeros have real part above sigma at five values of sigma from 3/4 to 0.87. A single split at 0.85 already closes k = 8.
For every integer n >= 1 there is a prime p with n^9 < p < (n+1)^9grade proved, given the input; every numerical step enclosure-carrying; unreviewed
against k = 86 for every n, unconditional (Lee, arXiv:2602.14340, 2026)
Legendre's conjecture asks for a prime between consecutive squares, and it is open. For a k-th power version valid for every n, the best unconditional k was 86 as of 2026. Given the 7/8 half-plane the explicit formula for primes has an error of size x^(7/8) (log x)^2, which beats the gap (n+1)^k - n^k, about k x^(1 - 1/k), exactly when k >= 9.
For every nonprincipal Dirichlet character chi mod q >= 3, the least n with chi(n) not in {0, 1} is at most (log q)^8, so the least quadratic nonresidue mod p is at most (log p)^8; every odd composite n has a Miller-Rabin witness at most (0.7 log n)^8grade proved, given the input; enclosure-carrying; unreviewed
against OpenAI: least quadratic nonresidue at most C (log p)^32, with C not stated
If chi is a character mod q that is not identically 1 on the units, how far must one search to find an n with chi(n) != 1? Under GRH the answer is about (log q)^2 (Ankeny, Bach). With a zero-free half-plane Re s > theta the classical exponent is 1/(1 - theta), which is 8 here. The hunt proves it with constant 1: n <= (log q)^8 for every q >= 3, tight at q = 3, and (0.7 log q)^8 for q >= 5.
The least prime congruent to a mod q, for (a, q) = 1, is at most C(eps) q^(7/3 + eps), with C(eps) effectivegrade proved, given the input and the Chen-Gupta-Li density estimate (arXiv:2507.08296, a preprint); 12/5 from refereed inputs alone; unreviewed
against L = 5, unconditional (Xylouris 2011 and 2018)
Linnik proved that every reduced class mod q contains a prime below q^L for some fixed L; the best unconditional L is 5. Under GRH it is 2. With every zero at real part at most 7/8, the Siegel zero, the Deuring-Heilbronn repulsion and the log-free density estimates all drop out of the argument, and L is governed by the zero-density exponent for the family of characters mod q on 1/2 <= sigma <= 7/8.
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-10-31 | Owner decisions: lambda_dh_exact P4 refuted; dbn_pt_height gap… | 2893bd93 |
| 2026-10-31 | Land #383 with corrections: the deep predictions were not a… | 1bf7c1ef |
| 2026-10-31 | hunts/dbn_pt_height: land hunt #147 with RESULTS.md, dated… | e8b677f5 |
| 2026-10-31 | hunt #150 synthesis: dated corrections after checking claims… | 091f3b95 |
| 2026-10-31 | hunt #150 spectral_operator challenge: set the Arb traps on… | 27f0ba8a |
| 2026-10-31 | hunts/dbn_pt_height/evaluator: stage 2 of the DH gate, run as… | 43d50047 |
| 2026-10-31 | weil_dh_line: one Lean def per matrix row | fed73cac |
| 2026-10-31 | hunts/dbn_pt_height/evaluator: preregister stage 2 of the DH… | de7cd593 |
Branches carrying commits that are not on main, read off git.
| branch | what | last |
|---|---|---|
| cursor/scrub-checkpoint-home-path-79ca | lab: scrub machine-local path from CHECKPOINT.md | 2026-11-06 |
| claude/vigilant-rubin-gzav0b | hunts/wide_search: drop a personal GitHub account name from… | 2026-10-31 |
| docs/weil-degeneracy-briefs | docs/reviews: four agent briefs for the weil-degeneracy… | 2026-10-30 |
| hunt/weil-degeneracy | docs/reviews: four agent briefs for the weil-degeneracy… | 2026-10-30 |
| hunt/plocal-rivals | Hunt #149 plocal_rivals: close the zero census, three PARI… | 2026-10-21 |
| codex/palomar-root-package | Verify root package with pinned original Palomar pipeline | 2026-10-01 |
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,386 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.35.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 | 21 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 3 evaluations 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. 329 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. |
The working paper, the obligation ledger, every hunt, every frozen protocol and every correction, in full rather than summarised.
915 documents, 220,517 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 →