Every finish stays tiled. Choose a look to replay the reveal, or mix the texture, palette and reflections yourself. Hold start freezes the starting shape. Replay opening brings it to life. Drag Opening to inspect any pose.
ζThe canyon starts as the sampled zeta surface. Other looks reshape it for the reveal. Height shows log modulus, clipped at ±3. Both halves separate around the sample nearest Re(s) = ½. Motion, colour and thickness are visual styling.
From the lab’s own grid.
The pale staircase jumps at primes and their powers. Scroll to add waves and watch the teal curve find those jumps. This is Chebyshev's function ψ(x): it climbs by log p at every prime power. Riemann's explicit formula writes it exactly, as a smooth term minus one wave per zero. Here the sum runs over the first zeros of zeta and nothing else.
Twelve zeros. The sum is already a wave that leans into the staircase. With no zeros it would read 98.16 at x = 100; the true value is 94.0453.
A hundred zeros, and the corners begin to emerge near 73, 79, 83, 89 and 97, and near 81 = 3⁴. The curve approaches the staircase, with ripples from the finite sum.
Five hundred, and the edge near 97 sharpens. In the lower view, waves from the zeros reinforce each other near the logarithms of prime powers. Residual oscillations remain: this is a finite approximation to the explicit formula.
The first 1,000 zeros, mpmath.zetazero, from the tree. The lab’s script prints the same table at 30 digits; document 04 derives the identity.
The laboratory
One person. A team of agents. Every proof checked.
Everything above was computed from the lab's own tables. Thomas Lince opened Zeta Lab in August 2026 around
a question it states in its own words: how much legitimate research a very
small human organisation can produce when generation is cheap, scepticism is architectural and verification is
systematic. This page is what it has produced so far.
The division of labour is fixed. Coding agents, Claude Code, Codex and Antigravity,
write the code and the Lean. Harmonic's Aristotle searches for proofs of
named subgoals and returns Lean. The Lean kernel checks every step of every theorem. A person directs the work and
decides what counts as a result. One rule, written down and testable, keeps
the machines in their place: a model is used only where its output is checked against an oracle that is not a
model.
The lab's own front page says that finite numerical agreement does not settle the Riemann Hypothesis.
A surprising result has to be checked, with its exact scope kept visible. What the lab does have is
a course of 37 documents from the harmonic series to the
frontier, instruments that measure rather than assume, a battery of controls
every claim has to survive, and theorems that an outside registry has since rebuilt from scratch.
A zero is a point where the function’s value is zero. The Riemann Hypothesis places all its nontrivial zeros on one line: real part exactly one half. This is the strip 0 < Re s < 1 up to height 120, and the guide draws their locations.
Hardy's Z is real on the line. Its sign changes locate simple zeros. Below height 100 there are 29 crossings, and the argument principle, which counts zeros in the whole strip, also gives 29. None are off the line.
Now the rival. The Davenport-Heilbronn function has the functional equation, real coefficients and a real Hardy-style Z, everything zeta has except the Euler product.
It has a zero at 0.8085… + 85.6993…i, off the line, and the mirror image of that zero under s → 1 − s. So symmetry alone does not give the Hypothesis, and that makes this function the lab’s standing rival: any property of the zeros it shares with zeta explains nothing about zeta. The lab formalized its analytic properties in Lean, and the registry rebuilt the build. The off-line zero shown here is numerical, not part of that registered theorem.
The lab’s script polishes the off-line zero to a verified value; document 22 uses the rival to measure what a detector can see.
Verified outside the lab
3 results, rebuilt by a registry
Within three weeks of opening, the lab had results worth checking by somebody else. On 18 August 2026 the Lean
FRO and ICARM opened Palomar, a registry of Lean-verified mathematics. The lab submitted
three days later, and 3 of its results now have registry entries. For each one Palomar fetched the
pinned commit, rebuilt the whole development on its own hardware in a sandbox, replayed the proofs through Lean's
kernel and the independent NanoDa kernel, and checked that the theorem advertised is the theorem proved. This checks the build and the statement. It is not peer review, and no person has read any of
them; document 32 records what the check adds and what it does not.
In August 2026 Alpoge and Furman proved, with a proof discovered by Claude and
a Lean development the lab builds on, that more than two thirds of the zeros are simple
and on the critical line, a proportion H = 0.6725…. Ainta pushed the constant higher on
a certificate, a seven-point inequality that an interval-arithmetic program accepts rather than proves. The lab
generalised the argument to n points and then, at three and four points, proved the inequality inside Lean. The
results are 0.67273… and 0.67284…, both proved without a certificate hypothesis.
The four-point figure improves the source theorem under the same axioms.
An identity original to the lab, in the setting of the same paper. Over the admissible class of windows the
constraints cost nothing: the supremum of the window functional is exactly <1, A⁻¹1>, the value of the
unconstrained problem. Three theorems; the existential form carries no hypothesis.
The rival from the strip above, as a Lean object. No library the lab could find had it, so the lab built it:
the character, the combination, entirety, real coefficients and the completed functional equation, with the
convention-sensitive constant derived inside Lean rather than copied from a table.
03 · Random matrices
Look at the gaps
Each bar counts gaps of a given size between neighbouring zeros. The spacings are rescaled so one is the average. Scroll to compare the measured pattern with two different models.
Independent points would pile up at small spacings. The zeros do the opposite: the histogram starts at nothing and rises. Two zeros are rarely close together.
The curve is the Gaudin law, the spacing distribution for the Gaussian Unitary Ensemble. This instrument uses 10,141 spacings from 10,142 zeros, up to height 10,000. Their Kolmogorov-Smirnov distance from that law is 0.0287.
Poisson, the law of independent points, is at 0.3065, 10.7 times further away. The zeros repel the way eigenvalues do. Whether they are the eigenvalues of some operator is the Hilbert-Pólya idea: a strategy, not a theorem.
The dots are zeros. The slider changes flow time. Ξ is the entire function whose real zeros are the zeros of zeta on the line. Put it under the backward heat equation and its zeros move.
Backwards in time they attract. As t falls, the smallest gap among the first 10 zeros closes.
Forwards they repel and spread out, and once they are all real they stay real. De Bruijn and Newman's constant Λ is the threshold, the infimum of the times at which every zero is real.
Λ ≤ 1/2 is de Bruijn's theorem, Λ ≥ 0 is Rodgers and Tao's, and the Riemann Hypothesis is exactly the statement Λ ≤ 0. So the Hypothesis says Λ = 0: the zeros of zeta sit at the exact edge of criticality.
Tracks from the lab’s cache at 6 flow times, interpolated; displacement drawn at 25×. The lab’s script prints what is proved about Λ and by whom; document 05 is the chapter.
three theorems on one ruler · the two in teal are the lab’s unconditional improvements
05 · What is proved today
How much can we prove?
Nobody can prove that every zero is on the line. What can be proved is a proportion: at least this fraction of the zeros are simple and on the line. Three figures for it are theorems, and all three are on this ruler.
Alpoge and Furman's Theorem D, August 2026: at least H = 0.67250070… of the zeros, more than two thirds, unconditionally and in Lean.
Above it, in teal, the lab's two. 0.67273733… at three points and 0.67284701… at four, proved in Lean with no hypothesis, rebuilt and registered by Palomar. The four-point figure improves Alpoge and Furman’s unconditional constant under the same axioms.
The higher certificate-based bounds rest on a finite inequality that a program accepts rather than proves. The lab proved the passage from certificate to proportion in Lean, audited the certificates themselves, and found and reported a defect in the shared verifier. None of that is on the ruler, because none of it is a theorem.
The audits are in the record. None of this bears on the Riemann Hypothesis.
01 / The result
Independently rebuilt · Palomar Registry
A better bound on simple zeros.
The lab improved Alpoge and Furman’s unconditional bound for simple zeros on the critical line.
The finite inequality is proved inside Lean, under the same standard axioms, with no certificate hypothesis.
A credential usually hides this part. Here a result is not a result until it has survived an attempt to kill
it, and the attempts are public. The graveyard names
3 withdrawn results, each with why it was wrong and what caught it; the first,
blockpos 0.672529 (and siblings 0.6725124, 0.6725318), fell to an exact Gaussian-integer counterexample
in the lab's own review. 9 guards now exist because of specific incidents, and 8
of them have a mutant that shows they fire.
The lab also turned the method on itself. It built a general refereeing framework, ran four preregistered
experiments across two subjects and 74 agent runs, and found that the plain practice it was meant to improve was
never wrong, 37 for 37, while the framework was never better and cost 1.1–1.7× the tokens and 2.4–5.0× the tool
calls for the same answers. Nothing in the repository used it, so it was demoted rather than deleted, and
the verdict stays in the tree because the negative result is the useful part.
Two documents tell the rest: how five claims of zero structure died in one day, and
the director run, when the laboratory was pointed at itself and six of its own claims died.
the construction used u u* where the pinned upstream zero side uses u u^T; an off-line pair is the hyperbolic block 2m(xx^T - yy^T), whose interaction with the on-line part can be negative, and the proposed final additive inequality reads 9 >= 13
individual place contributions can sometimes be represented as norms, but the local pieces do not consistently carry the sign naive global assembly needs
the local-positivity hunt's own instruments; zeta.criteria face 1 is the in-tree counterexample to the coefficient-blindness universal (ROADMAP known gap #0) record
The stock
A growing stock of kernel-checked theorems
Beyond the registered results, the lab's Lean arm holds
1,178 theorem and lemma declarations, each checked by the kernel on every nightly run. Some
are classical theorems in their own right: Hardy–Ramanujan theorem and Mertens's theorems, proved here with no unproved step, and
Hardy's Z, the function crossing zero in chapter two.
Mathlib, the Lean community's library, lists those theorems as wanted and
unbuilt, 970 such entries at the lab's last survey. The proofs are in this tree
under the MIT licence, and anyone who wants them can port them. The lab's own table,
with status:
Mathlib entry
Declaration here
Status
Q5656674 Hardy–Ramanujan theorem
ZetaLean.HardyRamanujan.hardy_ramanujan
proved here; not ported, not submitted
Q1196729 Mertens's theorems
ZetaLean.Mertens.mertens_second_theorem
proved here; not ported, not submitted
Q205966 Critical line theorem
, (infrastructure only)
Hardy's Zsubmitted as mathlib4#42963; the theorem itself is not proved
Q1632301 Sturm's theorem
groundwork only
four support lemmas; the theorem is not proved
Now
What is cooking
Read off git when this page was built, from the public tree. Landed is the last
8 changes to reach main, one row per merge. Ahead
is the branches carrying work that main does not have yet, newest first. Only the
work directories count; the harness, the scripts and the lab's instructions to its agents are filtered out.
Each row links to the change itself.