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 whole closure split site by site, with coverage shown (216 shards; the assembly's declarations abstracted over the site theorems; every constant of their dependency closure checked). 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.

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.

Result	What it says	Previous best
Class numbers up to 1500 (hunt #124)	h(D) >= sqrt(q) / (10 pi log log q) for every negative fundamental discriminant D = -q, and with it the complete list of imaginary quadratic fields of each class number h <= 1500: 9,245,562 fields	h <= 100 unconditionally (Watkins, 2004); all h <= 1000, including even h, under GRH (Cremona-Sutherland, 2023, section 5)
Primes between seventh powers (October 8 extensions)	a prime between n^7 and (n+1)^7 for every n >= 1, given also Kadiri-Lumley-Ng's explicit zero-density estimate; audited by a separate agent, reviewed by no person	k = 9 from the theorem alone (hunt #126); k = 86 for every n (Lee, 2026); every n under full RH (Chamberland-Straub, 2026)
Primes between ninth powers (hunt #126)	a prime between n^9 and (n+1)^9 for every n >= 1, from the theorem alone	k = 86 for every n (Lee, 2026)
Small witnesses (hunt #125)	for every nonprincipal character mod q >= 3, some n <= (log q)^8 has chi(n) not in {0, 1}; every odd composite n has a Miller-Rabin witness <= (0.7 log n)^8	exponent 32, constant not stated (OpenAI)
Linnik's constant (hunt #123)	the least prime in every reduced class mod q is below C q^(7/3 + eps), C effective; 12/5 from refereed inputs alone	L = 5 (Xylouris)
The input itself (docs/38, section 7)	OpenAI's Lean proof rebuilt from the pinned commit; Lean's kernel and the independent NanoDa kernel accept it with only the standard axioms

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

Guide	For you if you want to…	First command
learn	see the classical machinery run at arbitrary precision	.venv/bin/python scripts/06_tour.py
refute	test a claim about the zeros against the control battery	.venv/bin/python scripts/23_gate_3_battery.py
certify	Lean proofs and interval enclosures	cd lean && PATH="$HOME/.elan/bin:$PATH" lake build
discover	run the conjecture funnel and see its measured hit rate	.venv/bin/python scripts/13_discovery_run.py --dry-run
evaluate	run an LLM against a proof-backed grader rather than an LLM judge	uv run --directory environments/bloch_certificate bloch-smoke
contribute	clone the lab, run a bounded agent hunt and return checkable findings	.venv/bin/python scripts/71_contribution_check.py hunts/<short-name>
adopt	(demoted, read harness/VERDICT.md first) the validation framework and why it was frozen	.venv/bin/python -m pytest -q -o addopts='' tests/test_harness_protocol.py

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 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, 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, 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, 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, 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:

tier	when	what	cost
checks	every push and PR	342 tests, stdlib + pytest only, no numpy, scipy, mpmath, no editable install, plus make_context.py --check	~7 s
tests	PRs and pushes to main	the fast tier with the real dependency set; asserts rigor.BACKEND is genuinely Arb before running, because the mpmath fallback silently drops the cross-check that licenses the word certified	~20 min
full	nightly, and on demand	the complete suite including slow, plus the Lean arm as its own job with a zero-sorry scan	up to an hour

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).

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.

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.