the record
zeta-lab, and what it has actually produced
01what it is
A computational and formal laboratory around the Riemann zeta function: reproducible numerics, adversarial falsification, and kernel-checked formalization.
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.
02why it is worth reading
A laboratory that generates candidates quickly is worth nothing without something that refuses the bad ones, and the refusing is the part that is hard to fake.
Lean reads a mathematical argument and rejects it if a step is missing. That is the strongest guarantee mathematics has, and until recently getting one meant years of specialist work.
03the full record
Everything the pursuit produced is published, including what did not work — the numerics, the falsification attempts, the Lean sources and the reading order.