We follow interesting problems. We explore several directions cheaply, feed the ones that produce something, stop feeding the ones that do not, and keep the loose ends we are not pulling so that choosing one direction does not mean forgetting the others.
The impulse is roughly what happens if we pull on this? Most of the time the answer is nothing much, which is why the record carries as many dead ends as findings, and why we would rather show you both.
The mathematics, the tests, the proofs and the evidence are public, because the point of publishing them is that a stranger can re-derive the numbers instead of trusting us. Results go up whether or not they flatter us.
Zeta is the first pursuit. There will be others.
The results are public. The process is not.
Everything needed to check a claim is in the open: the mathematics, the proofs, the tests, the corrections and the claims that did not survive.
One consequence, because a reader counting commits here could otherwise draw the wrong conclusion in either direction: this repository is the research record, not the whole laboratory. Every figure on this site counts published research, and none of it counts the work on the other side of that line.
Every page here is generated from the repository by
scripts/72_site.py: theorem counts from the Lean sources, module
titles from their own header blocks, the public surface from the Python AST,
withdrawn results from the graveyard ledger, experiments from the gate evidence,
open lines from git. Nothing is maintained by hand, so nothing here can quietly
disagree with the tree it describes.
That rule earns its keep. A page compiled by hand on 12 August was still advertising our validation framework as this laboratory's strongest capability on 13 August, the day our own experiments demoted it. A generated page stays current by construction.