Zeta Lab

A computational and formal workbench around the Riemann zeta function.

Its purpose is that you can check it yourself: clone it, run it, and re-derive the numbers rather than take them. Every number claimed in a docstring is pinned by a test, identities are exposed as measured defect functions rather than assumed, and the Lean arm is checked by a proof kernel.

Original mathematics toward RH and useful intermediate results is the research objective. Attempting a proof is allowed; claiming success requires the complete checked argument. Finite numerical agreement does not settle RH, but rigorous finite certificates and computational discovery can contribute to proofs within their stated scope. See ALIGNMENT.md and the scoped failure catalogue.

The public reading surface is <https://zeta.teal-sea.com>: what has been established, what is still a candidate, and what was withdrawn. Every figure on it is derived from this tree at build time rather than typed in, so it cannot quietly disagree with the repository it describes. Its generator lives in a separate repository; this one holds the record, not the presentation of it.

Current results (October 2026)

RH to height 100, kernel-checked (docs/45, hunt #137). A Lean proof about Mathlib's own riemannZeta: every zero with 0 < Re rho < 1 and 0 < Im rho <= 100 lies on the critical line and is simple, and there are exactly 29 of them. Lean's kernel accepts it from a clean build with zero sorry and only the three standard axioms, and the independent checker con-ron --verified accepts the exported proof as well. A fresh replay of the whole closure by Lean's own kernel (leanchecker --fresh, rerun without a time cap on 2026-10-26) accepts it too. The independent NanoDa kernel stopped at the laboratory's memory cap without a verdict. No outside computation enters as an axiom or hypothesis; generated numerical data is checked by the kernel. RH has been verified numerically far higher; this is a finite theorem, reviewed by no person, and says nothing about RH itself.

The Davenport-Heilbronn zero, kernel-checked (hunt #145, rung 3 of the Lean ladder). One Lean theorem, davenport_heilbronn_strip: some entire function with zeta's kind of Dirichlet series and functional equation has a zero in the open critical strip, off the line. The witness is the Davenport-Heilbronn function DH, and the zero lies in the closed square of half-width 3/64 about 0.808517 + 85.699348 i (dh_zero_located; Spira's zero, 1994). dh_separation_hundred adds that it lies below height 100, where riemannZeta has no off-line zero (hunt #137). Lean's kernel accepts them with zero sorry and only the three standard axioms, from 215 site theorems compiled on GitHub Actions and one assembly; planted one-unit faults are refused. A fresh replay of the whole assembled closure by Lean's own kernel (leanchecker --fresh, 2026-10-27, 1.57 million constants in 7 h 17 min) accepts it too; that is a re-check by the same kernel. The independent checker con-ron --verified accepts the dependency closure of the 18 final declarations (675,388 constants), split site by site, with coverage shown (216 shards; the final declarations checked in a form abstracted over the site theorems). The constants outside that closure were replayed only by Lean's own kernel. The grade is kernel-checked, pending external verification. The older davenport_heilbronn_statement is also met by the trivial zero s = -1 (lean/ZetaLean/DHTrivialZero.lean), so it carries none of the result. It shows that the functional equation alone cannot give RH. It is not progress toward RH.

Where Li's criterion first fails for Davenport-Heilbronn (hunt #151). lambda_{328997}(DH) < 0, and lambda_n(DH) > 0 for every 1 <= n < 328997: the first negative Li coefficient of DH, at exactly the index hunt #128 extrapolated, in 0.46 core-hours against #128's estimate of 20,000. Every step carries an Arb ball, and two radii agree at every n <= 500,000, so the grade is hardened. A pre-registered rerun with an mpmath.iv evaluator that shares no evaluation code with Arb reproduces the same n* and every sign. What both routes still share (the DFT, the aliasing bound, the tracking, the admissibility certificate) is named in its record. It is not kernel-checked and not reviewed outside this lab. Like the result above, it is about a function with no Euler product and says nothing about RH.

The rest of the October record, each with its grade and its doors, is in the case log at the top of hunts/README.md. That includes measured and hardened studies of the Weil functional at the Davenport-Heilbronn line (hunt #146 and the weil_propagation lanes) and of how its arithmetic side degenerates (hunts #155 to #157, measured), two probes of where OpenAI's 7/8 comes from (hunts #139 and #148), a ball-arithmetic localization of a sign change of pi(x) - li(x) at published parameters (hunt #152, not a new record), and the opening of Gabcke's Riemann-Siegel remainder for Lean (hunt #154).

On 2026-10-06 OpenAI released a proof that no Dirichlet L-function, zeta included, has a zero with real part above 7/8. This laboratory rebuilt its Lean proof on its own compute, two independent proof kernels accepted it (docs/38), and five results were then built here on top of it. Four (hunts #123 to #126) are proved, given OpenAI's theorem, with every numerical step carried by ball arithmetic. The fifth, a prime between consecutive seventh powers, also needs a published explicit zero-density estimate; it is a written conditional candidate that has passed an independent written audit by a separate agent of its author's model family. None has been reviewed by any outside mathematician, and none is formalized in Lean. Statements, proofs in outline, what each one beats, and how to check it: docs/39.

One of them runs in about three seconds:

.venv/bin/python -m hunts.qrh_class_number.run_search 100 48611613 /tmp/cn100
# 42,272 fields: Watkins' complete lists for every h <= 100, reproduced given the theorem

Where to start

Thirteen worked demonstrations, the figure gallery, the repository map and the standing list of limitations are in docs/36-what-you-can-run.md. The docs are a single course and 00 → 01 → 02 → 03 → 04 is one argument: start at docs/00-orientation.md, and docs/README.md lists all forty-eight with one line each.

Quickstart

git clone https://github.com/teal-sea/zeta-lab && cd zeta-lab
python3 -m venv .venv                # Python >= 3.11
.venv/bin/pip install -r requirements.txt
.venv/bin/pip install -e .
.venv/bin/python scripts/06_tour.py  # the whole story in ~90 seconds, six acts

Dependencies are ordinary: mpmath, numpy, scipy, matplotlib, sympy, plus python-flint for the ball-arithmetic backend. Expensive computations cache under data/, so second runs are fast.

Earlier results

The August and September record. Each stands in its own lane; none depends on the October input above.

The four-point theorem, strengthened

The lab's four-point theorem now has coefficient (14400000 H - 17240)/14366681, approximately 0.6728603588, with H = 3/2 - cot(1/sqrt(2))/sqrt(2). For every positive epsilon, the proportion of simple critical-line zeros among all zeros in (T, 2T] is at least this coefficient minus epsilon for all sufficiently large T. This improves the registered four-point coefficient below; it is not RH.

The recorded lab build at 5522b963 has 49 successful receipts, zero sorry warnings, and only the standard three axioms for all six advertised declarations. Its source hashes were checked during integration. This result is kernel-checked at the pinned revision, pending external verification, and not yet registered with Palomar. The current registry requires a toolchain and module-format port, tracked in Palomar preparation. The registered results below remain unchanged.

Registered with Palomar

Three results here have been rebuilt and kernel-checked by someone other than their author. Each was submitted to the Palomar Registry (https://palomar-registry.org/), the Lean FRO / ICARM registry of Lean-verified mathematics, which fetched a pinned commit, rebuilt the development from scratch on its own hardware inside a sandbox, and replayed the proofs through Lean's kernel and the independent NanoDa kernel.

PALOMAR-2026-08-25-000005 (https://palomar-registry.org/entry?id=PALOMAR-2026-08-25-000005&version=1), the n-point simple-zero bound (lean/bridge/). The parametric theorem and four instances. The three- and four-point instances are unconditional: their finite certificates are proved inside Lean, by interval cell lemmas over rationals rather than accepted from an external program, so the theorems carry no certificate hypothesis.

Φ₄ = (906250·H − 1085)/904171 = 0.6728470197… Φ₃ = (149000000·H − 99200)/148800133 = 0.6727373345…

built on anthropics/zeta-23-lean (arXiv:2608.13637), whose Theorem D gives H = 0.6725007036… unconditionally; the step from 41.6% to H is theirs and is much the larger piece of work. #print axioms reports exactly [propext, Classical.choice, Quot.sound]. The eight-point instance keeps its certificate as a named hypothesis and is registered as conditional.

PALOMAR-2026-08-21-000004 (https://palomar-registry.org/entry?id=PALOMAR-2026-08-21-000004&version=1), the source-admissible strong closure (lean/). With A = I + T the Fredholm operator whose kernel is the Farmer–Gonek–Lee form factor F1 on I = [-1/2, 1/2], w = A^-1 1 and c* = <1, w>, over the compactly supported monotone admissible class v(s) = phi(Ls)^2:

sup <1,v>^2 / <Av,v> = c*, and inf <Av,v> / <1,v>^2 = 1/c*.

The upper bound is energy Cauchy–Schwarz and is classical. The content is the reverse inequality: the class constraints do not lower the supremum, proved by exhibiting an explicit endpoint-tapered family whose quotient converges to c*. Scope: a statement about a Fredholm operator on an interval and a class of test profiles. It says nothing about the zeros of ζ, nothing about RH, and asserts no numerical value for c*.

PALOMAR-2026-08-21-000012 (https://palomar-registry.org/entry?id=PALOMAR-2026-08-21-000012&version=1), the analytic half of Davenport–Heilbronn (lean/palomar-dh/). The registry classifies it source-based: it formalizes an existing theorem rather than establishing a new one.

None of this is peer review. No person read any of them.

Check any of them yourself:

cd lean/bridge && PATH="$HOME/.elan/bin:$PATH" lake build V2Challenge V2Solution
# Solution builds sorry-free; Challenge carries one deliberate sorry per advertised
# statement, which is what the Palomar format requires.
bash scripts/palomar_stage.sh              # from the repo root, checks all four paths

Conditional results, and where the method stops

Certificate-based figures above H exist, here and elsewhere, and every one of them assumes a finite certificate that has not been proved. They are claims, not theorems. This tree's best is an eight-point certificate at 0.6730529829…; the highest published anywhere is 0.6734164909… (AMTOPA/zeta-exact-pressure), whose artifact returns INCONCLUSIVE 1.19e-07 short of its own target when run at its own pinned tip, with all six of its interval tables reproducing byte for byte (hunts/amtopa_ceiling/). trmdy's full 2,168,370-box interval run was reproduced here node for node with no soundness defect found.

Every conditional figure above H, including this tree's, rests on an analytic bridge that no person has reviewed. Φ₃ and Φ₄ do not.

The pressure-certificate family built on the Montgomery–Taylor window saturates at sup Φₙ ≤ 0.675142509660254, against a configuration ceiling of 0.6818286874638 (hunts/family_wall/). Adding points cannot close that gap. The argument was audited adversarially by an independent model working from a blank directory, which found two repairable defects in the write-up and could not break the result.

A separate artifact with its own ledger: the gap-census transplant in hunts/frontier_math/ carries a candidate reading of record of 0.6725106958, graded step by step in its PROOF-LEDGER.md. It is a candidate on a different chain, not one of the certificate figures above, and it moves only when its ledger does.

Negative controls, and one framework that did not earn its keep

The control practice stays: challenge a proposed implication with a rival that satisfies its complete hypotheses but lacks its conclusion. The Davenport-Heilbronn function shares important analytic symmetries with zeta and has off-critical zeros; zeta.epstein.battery exposes it and other rivals. Passing a shared intermediate lemma does not invalidate an argument using additional arithmetic. The proof must justify that extra structure, and a failed rival computation does not count as excluding the rival. See ALIGNMENT.md section 5 and docs/08 section 4.

harness/ generalized that into a subject-independent framework with pluggable departments. In August 2026 it was tested against the practice it was meant to improve: four preregistered experiments, two subjects, 74 agent runs. The harness arm never outperformed the control, the control was 37/37, and at identical correctness the harness cost 1.1–1.7× the tokens and 2.4–5.0× the tool calls. Live hunts had meanwhile reimplemented the same four control roles by hand rather than import them.

It is therefore demoted, not deleted: the ledgers under harness/ (dead ends, guards, reviews) have a live consumer in scripts/70_lab_state.py and stay as ordinary bookkeeping; the framework is frozen. The full record, including the protocols frozen before each run, is harness/VERDICT.md and harness/gate-evidence/.

The negative result is kept because it is the more useful artifact. It also supplies the rule in AGENTS.md: do not build an abstraction without naming the live thing that will consume it.

Checking the whole thing

Continuous integration runs on every push, in three tiers cut by measured cost:

That CI is young and has already earned its place: its first complete run found a PROVED formal record citing a kernel build older than the file it certified, stale for six days, because until then nothing ran the suite unless a human remembered to (#20 (https://github.com/teal-sea/zeta-lab/issues/20)).

Locally, .venv/bin/python -m pytest -q -m "not slow" is the fast tier.

Open observations live as issues. Something measured, noticed, broken or bounded is a fact about the subject or about this tree, and it is true whether or not anyone is pursuing it. Those are filed openly rather than kept in a backlog file, see the open issues (https://github.com/teal-sea/zeta-lab/issues).

What this is (and is not)

This is an instrument for exploration, proof attempts and formal mathematics around zeta, RH and useful intermediate questions. It reconstructs, tests, connects, challenges and develops ideas. The current mandate is in ALIGNMENT.md; the previous blanket ban on RH attempts is superseded. Constructive research and careful verification support each other.

There are two certainty regimes, and they are not the same claim. The numerical machinery in zeta/ is accurate, and zeta/rigor.py alone may say certified, for quantities whose every step carried an enclosure. lean/ is the second: a Lean 4 + Mathlib project whose theorems are checked by a proof kernel rather than measured, and nothing there counts until it compiles with zero sorrys. Ordinary mathematical derivations state their assumptions and review status separately. No result is upgraded by a policy change.

Pointers

• ROADMAP.md records current project decisions and links the preserved dated history. Read it before planning work.
• AGENTS.md is the shared operating context for coding agents: setup, house rules, naming traps and tests. It links to CLAUDE.md, so both agent entry points read the same instructions.
• ALIGNMENT.md states the research mandate, evidence rules, scoped treatment of negative conclusions and owner-reserved decisions.
• CONTEXT.md is the generated index of the public API, the document list, the script list and test counts. Regenerate it with .venv/bin/python scripts/make_context.py; never edit it by hand.
• .venv/bin/python scripts/make_figures.py --quick regenerates figures/.

License

MIT, see LICENSE.