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.

Twelve 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 thirty-seven with one line each.

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.

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

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.

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.

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

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.

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.

• 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/.

MIT, see LICENSE.