Using ldgr we tightened a published bound on the Riemann zeta function

What was missing

In August 2026, Alpöge and Furman published a proof that more than two thirds of the nontrivial zeros of the zeta function are simple and on the critical line, 67.25% after optimisation. Tucked into §7.2 of that paper is a second, quieter result. They show that the entire class of methods their proof belongs to can never do better than about 68.18%, no matter how cleverly anyone applies it.

That ceiling is established by exhibiting what is called a witness. It is a strange object: a fictional world, built to look exactly like the zeta function through the only window the method has, but containing far fewer simple zeros than we believe zeta actually has. If the method cannot tell that world apart from the real one, it cannot prove anything stronger than what is true in that world. The witness caps the method.

Here is the gap. Their witness rests on a numerical certificate file that is not distributed. It is not hidden, and the paper says so plainly, but the file is not in the repository and there are open issues asking for it. Everything downstream of that file is checked inside Lean's kernel. The file itself is verified outside Lean by interval arithmetic that nobody else can rerun.

So the 68.18% ceiling is a number the mathematical community has to take on trust. Not because anyone is being cagey, but because the artifact needed to check it was never published.

We wanted to see whether we could close that gap from the outside.

What we did about it

A witness is a probability distribution over point configurations. Each configuration is a set of points on a circle of circumference 256, each point marked 1 or 2, with the marks summing to 256. A mark of 2 means two zeros sitting in the same place, which is to say a non-simple zero. The mixture has to reproduce the pair correlation statistics that zeta is known to have, which pins 255 linear constraints on it. Subject to those, you want as few simple points as possible.

That is a linear program with infinitely many columns, one per configuration, so you solve it by column generation: keep a manageable pool, solve, ask the dual which configuration would help most, find that configuration, add it, repeat. The hard part is the “find that configuration” step, which is a non-convex search over point positions and mark assignments.

We ran that loop for about a week. The pool grew to roughly 700,000 configurations. The final witness uses 257 of them, with weights that are exact rationals.

Our certified value is 0.681810782 against their 0.681828687, which is below theirs by 1.79 × 10⁻⁵. A lower witness is a stronger obstruction. It says the method class is even more limited than the published result establishes.

Then we did the part that we think matters more. Their ceiling_law256 theorem is stated for their own law, but it is proved through a generic lemma, so a different witness slots straight in. We emitted our law in their certificate format, instantiated their theorem on it, and had Lean's kernel check the result:

LawHD256_check     depends on axioms: [propext]
lawHD256_rows      depends on axioms: [propext, Classical.choice, Quot.sound]
ceiling_lawHD256   depends on axioms: [propext, Classical.choice, Quot.sound]

Three standard axioms, no sorry, the same profile as their own theorem. LawHD256_check passes by decide +kernel on propext alone, which means Lean independently re-verified all 256 row enclosures and both edge-bound inequalities as integer arithmetic.

The mathematics is entirely theirs. We supplied a better witness and made it checkable. As far as we know this is the first kernel-verified bandwidth-one ceiling that anyone outside the original author group has been able to produce, and the reason is simply that we are the first people to have a certificate we could feed it.

Ours is an exact rational that anyone can re-check in about four seconds with no dependencies.

Now the part that actually sells the tooling

Here is the number I keep coming back to. Over this project we recorded 79 facts in our research ledger. Seventeen of them were later contested, rejected, or superseded. More than one in five.

That is not a bad hit rate. That is what research looks like when you write things down properly. The alternative is not being right more often. It is not finding out you were wrong.

A few of the ones that stung.

We proved a whole family of solutions was exhausted. We were wrong. We ran 20,000 randomised draws through a generator, found zero improving candidates, and formally recorded the family as dead, which by our own pre-registration rules then blocked further work on it. Airtight, except the sweep was missing one step that every other code path in the project applied. Same generator with that step restored: 25 hits out of 301, twelve of them clearing the bar we had registered in advance. We had not measured an exhausted family. We had measured a crippled tool.

The adversarial review that caught this also noticed that 25% of our draws were being silently discarded by an uncounted guard, so “20,000 draws” was really about 15,000, and skewed. The verdict had to be formally overturned, the fact rejected, and the block lifted. All of that is in the record with timestamps, which is exactly why it was a ten minute correction instead of an argument about what we had meant three days earlier.

We nearly shipped a result that was pure noise. An A/B test came back with the treatment arm 2.16 times better than control, comfortably past the 1.25 times threshold we had registered before running it. Great result. Except we had also registered a second condition, and it failed. When we looked, only 2 of 2,600 accepted columns had actually come from the treatment. The 2.16 times was run to run variance. If we had registered the headline metric alone, like a reasonable person under time pressure would, we would have written it up as a breakthrough.

Our own code lied to us about passing. A verification script printed “PASS” using a threshold left over from a previous experiment. The registered bar was ten times stricter and the run had missed it. The ledger was the authority and the code was wrong. Without a bar committed in advance, “PASS” is just whatever the script says.

The session problem, which is the one nobody warns you about

This project did not run in one sitting. It ran across many days, many machine restarts, and a long string of interruptions. Agents hit usage limits mid run. One hit a content filter false positive on what was pure combinatorial optimisation. The main working session itself was reset more than once. On one occasion a search process ran productively for 68 hours and then died, and the only sign of it was a truncated log line.

This is the part of long running computational research that nobody puts in the methods section, and it is where most of the real time goes. Not the compute. The re-establishing of context after something breaks.

What the ledger gave us was continuity that did not depend on any session staying alive. When work resumed, the state of the investigation was a query, not a reconstruction. Which hypotheses had been registered, which had verdicts, which facts were accepted and which had been refuted and why, which directions were formally closed and therefore should not be retried. Every artifact carried a checksum and a link to the run that produced it.

Concretely, after one reset we came back to a ledger that said a particular family of solutions was closed, with the experiment that closed it, its pre-registered criteria, and its verdict. That saved re-running a day of search. Later, when that verdict turned out to be wrong, the same record is what made overturning it a clean operation rather than a debate.

That durability is the whole point of it. The ledger is a store, not a session. Conclusions, evidence, verdicts and checksums live in it independently of whatever process produced them, so nothing we established was ever contingent on a particular run staying alive. Over a project this long that mattered more than any single result did.

What the tool did, and what it did not

Let me be careful here, because the honest version is more persuasive than the marketing version.

ldgr did not find the witness. It did not suggest the change of representation that unlocked the deep search, or the dual stabilisation trick, or any of the mathematics. Column generation, a lot of CPU hours, and a lot of dead ends found the witness.

What the ledger did was stop us keeping things we should not have kept, and remember what we had established when the sessions running it fell over.

The mechanism that mattered most was mundane. You cannot record a fact as accepted on secondhand evidence. Three times we tried, and three times it refused and told us to go read the primary source. One of those refusals forced us to re-derive an identity ourselves rather than trust a report of it, and in doing so we discovered that a claim we had been building on for hours was refuted by a two line duality argument. That claim had already shaped our search strategy. We would have kept going.

Pre-registration did the rest. Committing pass and fail criteria before a run, with a hash of the definition so later edits are detectable, converts “did it work?” from a judgement call into a lookup. When we amended an experiment's parameter range mid flight, for the legitimate reason that the original range turned out to be numerically inert, the drift check fired and made us disclose the change and the reason on the record. That is the difference between amending a protocol and quietly moving a goalpost.

There is a pattern we only saw because everything was logged with provenance. Numbers measured against a stale optimisation state systematically overstate. A weaker state leaves more slack for any perturbation to look good against. Five separate reported improvements failed re-measurement at the current state. Once we had named it, we started re-measuring everything before acting, which killed several plausible directions early instead of after a day of work.

None of that is glamorous. All of it is the difference between a result and a story about a result.

The honest caveats

This is a ceiling on a proof technique, not a statement about zeta. It does not improve the 67.25% figure. That would need a better certificate, not a better witness. What it does is shrink the room left inside that method class and make the boundary independently checkable.

Our witness is certified but not optimal. We derived a rigorous lower bound of 0.679278 for this formulation, so there is likely still room below where we stopped. The search had not converged. It ran out of budget, and we were too keen to publish. We will keep pushing toward the lower bound and release those results when we have them.

Our certificate declares a band tolerance of 10⁻⁷ where theirs is 3 × 10⁻⁴⁰. That difference costs 1.95 × 10⁻¹⁰ in a downstream constant, four orders of magnitude below the margin by which the witness improves, so it cannot affect the comparison. It is still a difference and it should be stated.

Try it

ldgr-core is open source. ldgr-research is the adapter that adds what is described above: pre-registered experiments with drift-checked verdicts, an evidence gate with provenance classes, fact impact tracking, adversarial attack registration, and a ledger that outlives the session that wrote it.

We built it because we needed it, and this project is the hardest we have leaned on it. If you do work where being quietly wrong is expensive, or where the thing you are running takes longer than the thing running it, it may be worth a look.

The verification report, the certificate, the standalone verifier, and the Lean files are all in the repository. Everything in the number above is reproducible from public materials.

Bryan Carson, Hydra Dynamix. contact@hydradynamix.com

Disclosure, per the Leiden Declaration on AI and Mathematics: this work was carried out with substantial AI assistance (Claude, Anthropic), including the column generation search, the certification pipeline, the Lean instantiation, and the drafting of this post. Every quantitative claim above is machine-checkable from the artifacts. The adversarial reviews that caught our errors were also AI run, which is either reassuring or unsettling depending on your priors.