00
00. Orientation
Zeta Lab is a computational and formal workbench for studying the Riemann zeta function, attempting original mathematics toward the Riemann Hypothesis , and establishing useful intermediate…
The whole course, in the order it was written to be read. The early documents derive the mathematics line by line. The later ones are laboratory records: attempts run to their walls, a kill board of how hard problems die, and a catalogue of exactly why this one resists.
Two documents bound every claim on this site, and reading them first will save you the trouble of asking whether we are overselling. Why It Is Hard catalogues the known ceiling of every technique used here, including ours. How Hard Problems Die scores this problem against eight others and the mechanism that killed each.
Zeta Lab is a computational and formal workbench for studying the Riemann zeta function, attempting original mathematics toward the Riemann Hypothesis , and establishing useful intermediate…
Or: "is the harmonic series / Riemann-sum thing actually connected to the zeta function and to derivatives?", yes, and here is exactly how.
"Can you model the theta function with a differential equation?"
Riemann's functional equation is not a coincidence you verify afterwards; it is a change of variable.
The payoff of docs/02-theta-heat-and-modularity.md. There we watched heat flow produce Xi. Here we run heat flow on Xi and ask how the zeros move.
Or: the spectral dream. Why "there ought to be a differential equation behind this" is the right instinct, why nobody has produced the equation, and why the zeros nevertheless behave…
A curated catalogue of statements exactly equivalent to RH, with honest notes on which ones have ever gone anywhere.
The mathematical tools in this repository have proved many useful statements. Their current estimates do not by themselves establish RH.
The sequel to docs/08-why-it-is-hard.md. That document catalogued why the existing tools provably stall.
"The explicit formula looks like modal analysis. So what is the structure, and who gets to tap it?"
A companion to docs/09-new-ontologies.md. That document surveyed the "new objects" landscape and docs/10-trace-formulas-and-connes.md slowed down on the trace-formula corner; this one slows…
docs/08-why-it-is-hard.md catalogued what fails. docs/09-new-ontologies.md described the one time a rebuild worked.
The moments programme starts with a data contract, not a formula. The lab's local cache reaches only the low thousands in height; the external tables that matter live at much larger indices…
A companion to docs/12-how-hard-problems-die.md. That document is a kill board: eight problems, the mechanism that killed each, and RH scored against them.
The goal of the current sprint is to pass the Counting Gate. To do this, we must build a computational model of the Poisson-summation map on the Adelic Schwartz space, and demonstrate that…
A methods retrospective. Everything in docs/00–16 is about the mathematics; this document is about the refereeing.
A session's worth of deliberately improbable attacks on RH, each pushed until it either produced something measurable or hit a named obstruction. None of them advance RH.
A side project, and a probe rather than a department, see §6, which is the most useful part of this document because it is the part that says no.
The architectural record of the 2026-08-09 build: what was latent, how it was attacked before it was built, what survived, and where it stops.
Status when this file was committed: pre-registration only. No result in it. Everything below §5 was written before the gate existed, before any case was run, and before any number was…
Abstract The Riemann Hypothesis possesses numerous mathematically equivalent statements (Li's Criterion, Weil Positivity, Mertens' Conjecture, etc.).
Status of this file when it was committed: pre-registration only. Nothing in §§5–8 existed. No number below §4 had been measured.
An ontology attempt in the sense of docs/09 §4: propose a structure, push it at the gates, and record exactly where it bleeds.
2026-08-10/11. An operator handed the laboratory over with no theorem, no direction, and no assurance that the agenda was the right agenda.
ROADMAP.md ("The outside memos, triaged") records the decision; this document records what landed the same day, what each piece can and cannot claim, and where each one's honest edge is.
12 August 2026. A reading of the laboratory's current frontier work, written because the state changed four times in one day and the front page carries only the conclusions.
Disposition of the cheapest informative slice of meta/asymmetry-experiment.md. Run 2026-08-20, four checkers. Grade: measured, one run each.
Hunt #61 produced, so far as the literature search recorded in hunts/lambda_dh_bounds/NOVELTY.md reaches, the first quantitative bounds, from either side, on the de Bruijn-Newman constant…
A reading-course page about a threshold this laboratory did not discover. The threshold that governs the rightmost zeros of the prime zeta function is not this laboratory's result: it is…
Hunt #65 adjudicated two contradicting kappa = 2 tables in this repository and, in doing so, located the error that produced the disagreement. It is not in either table's code.
21 August 2026. On 18 August 2026 the Lean FRO and ICARM opened Palomar, a registry of Lean-verified mathematics, described by its own documentation as the analogue of a preprint server for…
Hunt #75 . Verdict: PRETTY BUT TRIVIAL for the note-to-hue question; the reformulation in section 9 is the one worth keeping.
Hunt #76 . Verdict: INTERESTING STRUCTURE, classical in substance. Measured in steps-per-octave, the Riemann zeros avoid the equal temperaments that tune prime-power harmonics and ignore…
Hunt #110, hunts/outband_intake/. Read hunts/outband_intake/RESULTS.md for the measurements and the doors.
Moved off the front page on 2026-09-05. README.md is an index, and AGENTS.md says so in as many words: "Keep README.md an index, not a manual.
This is the cross-hunt index of method. hunts/README.md logs each hunt by outcome; nothing there says which trick a later hunt could pick up. This file does.
1,183 declarations across 119 modules, checked
against Mathlib by a kernel that accepts no unfinished proofs, with zero
sorrys. The module breakdown →
The course above is the written-up part. Most of what I produced is working record: hunts, obligation ledgers, frozen protocols, routes opened and closed. It is all published, and it is all indexed. The library →