Erdos Minimum Overlap: Certifying Both Ends of a Gap

Last year I pointed a multi-agent research loop at a live numerical frontier in mathematics to see whether it could make progress that survives verification. This is the second dispatch. The honest summary is that the loop is good at producing candidate results and very good at destroying them, and that the destroying is where most of the value turned out to be.

The problem is Erdos' minimum overlap problem. Take the numbers 1 through 2n and split them into two equal halves. Slide one half against the other and count coincidences. Some shift always produces a lot of them. The constant mu measures how few you can force in the limit, and it has a clean continuous form: over measurable h on the interval [0, 2] with values in [0, 1] and integral 1, mu is the smallest achievable value of the largest overlap across all shifts.

Two things make it a good benchmark. Upper bounds are exhibitions: build an explicit h, evaluate it, done. Lower bounds are exclusions: rule out every h at once, which needs a certified relaxation. So the two sides are attacked by completely different machinery, and neither side can hide behind the other.

Everything I do on the lower-bound side sits inside a framework built by Ethan White, in "A new bound for Erdos' minimum overlap problem" (Acta Arithmetica 208, 2023). That paper is the load-bearing contribution: the Fourier reduction, the convex program, the reformulation as a second-order cone program so the dual can be written down explicitly, the divide-and-conquer over the parameter space, and the ellipse-extension argument that turns finitely many dual certificates into a bound over a continuum. My work is an augmentation of his program. It is worth being precise about that, because the rest of this post is about certificates failing, and none of the failures are his.

What I Actually Found

Three things, in descending order of how much they surprised me.

The upper bound most people are citing is not an upper bound. The number 0.380856 appears in an April 2026 paper as the best known value for mu, produced by an AI search system during an ablation study. I downloaded the construction it came from and re-evaluated it. The construction is real and feasible, but its actual objective value is 0.3809490 — worse than results from four years earlier. The gap comes from the search program reporting its bin count as n + 0.9999999999 instead of n, so the cell width used in the objective is understated by a factor of about one part in 4096. That deflates the reported score by exactly the 9.3e-5 that made it look like a record.

This is a search artifact, not a claim anyone made in bad faith, and the authors found it themselves: a commit to their repository a month after the paper says, in their own words, that they fixed "a potential hack possibility with n_points not being integer," and replaced the artifact with an honest construction scoring 0.3808677. Their search system was rewarded for a number its own evaluator would accept, and it found a way to make that number smaller. The paper has never been revised, which is the only reason this still matters.

The real record has a downloadable witness, and it now has an exact certificate. The Einstein Arena leaderboard's best entry is a 512-cell construction. I fetched it, confirmed it is exactly feasible, and certified it in exact rational arithmetic — no floating point anywhere in the chain from construction to bound:

That is the strongest upper bound on mu I am aware of that is backed by a witness anyone can check, and it improves the best previously certified value by 8.5e-6.

On the lower-bound side, the certificate under my own result was weaker than I had been claiming. More on that below, because it is the part I got wrong.

The State of the Problem

	Value	Source
Upper bound, certified here	0.3808590566	Einstein Arena witness, polished, exact arithmetic
Upper bound, widely cited	0.380856	not a bound — normalization artifact
Lower bound, best published	0.37912	Kim and Pilanci, ICML 2026
Lower bound, prior published	0.379005	White, Acta Arithmetica 2023
Lower bound, this project	0.3803954	full-space cover, every core anchor certified

The true gap is now [0.3803954, 0.3808591], about 4.6e-4 wide. My lower bound leads the published record by 1.28e-3, which is the one place this project holds a real lead — and Kim and Pilanci are working the same direction with the same rigor standard, so it is a lead with a clock on it.

The Part I Got Wrong

Recall the shape of the argument. You cannot search over all admissible functions, so you cover the space of a few summary parameters with regions, and in each region you exhibit a dual certificate whose objective value bounds mu from below there. The minimum across regions is the bound. What I added to White's program was Bochner moment-matrix constraints and polynomial-moment cuts, which raise the value in every region.

Each region's certificate is anchored at a number. In my code that anchor was the solver's reported objective minus 1e-5 — a haircut, chosen as a safety margin, on a value an interior-point solver printed. I had been describing that as rigorous. It is not, for two independent reasons I found this round.

The first is a routine bug with an unroutine consequence. The helper that extracts a "rigorous dual lower bound" from the solver log gates on a residual column, discarding iterations where the dual is too infeasible to trust. Its regex reads the fifth column of the solver's iteration table. The fifth column is the primal residual. The dual residual is the sixth. So the gate was checking the wrong quantity — for months, in the function whose entire job was rigor.

The second is worse because it was documented. The same function's docstring says that a strict bound needs zero dual residual, and that in practice one absorbs the residual "into a margin." No margin was ever absorbed. The returned value was the raw dual objective of a point that is only approximately feasible, which is not a lower bound on anything.

Neither defect makes the bound false. But "probably fine" and "proved" are different words, and I had been using the second one.

The uncomfortable part is that this is a step White did not skip. His Appendix II sets out a post-processing verification for exactly this hazard, and the paper states that every constraint inequality is satisfied by a margin exceeding the worst case for double-precision rounding — an a-priori feasibility argument, done by hand, in 2022. I had a stronger tool available, more compute, and a repository full of warnings about this specific failure mode, and I still shipped a margin that existed only in a docstring. The lesson is not that machine-assisted work is careless. It is that the discipline does not come free with the tooling.

Fixing It Made the Bound Better

The repair is a standard tool I already had and was not using in the main path: the Jansson-Chaykin-Keil a-posteriori bound. Given the solver's approximate dual, it computes a genuine lower bound on the program's optimum by explicitly charging for the dual's infeasibility and its distance from the cone, with every arithmetic step done in directed-rounding interval arithmetic. It does not trust the solver's status flag, its log, or its floating point.

Before this round, exactly two of the twelve anchor points in the binding region had such a certificate. I ran all twelve.

They all clear. And they clear by a lot — the certified value at each center came out above the convention it was replacing, by between 6.5e-6 and 2.6e-3. So the honest anchor is a stronger anchor than the invented one, and the fix tightened the bound instead of costing anything. The certified value can be used directly, with the dual read from the same solve, which is what makes the pairing valid.

The resulting bound, with every anchor in the binding region a theorem rather than a convention:

That is 1.12e-4 above where the bound started, and none of it came from new mathematics. Roughly a tenth came from replacing the guess with a proof; the rest came from pushing the discretisation to N = 48,000, which nobody had tried because an old note in my own repository recorded that scaling N "doesn't help" — a conclusion drawn from measurements that stopped at N = 40,000.

There is a second, weaker-looking number worth stating alongside it, because it rests on a much shorter chain. White proves a bound of 0.38 for seventeen of the eighteen regions outside the residual set — that is his Table 2, and he states the consequence directly: either mu is at least 0.38, or the extremal function's parameters lie in a small residual box. If I lean on his published theorem for those seventeen regions and supply only my own certified work for the remaining strip and the residual box, I get mu at least 0.380000, with nothing load-bearing except twelve interval-arithmetic certificates and a peer-reviewed paper. That is 8.8e-4 above the best published lower bound, and it is the version I would defend hardest — mostly because most of it is not mine.

What Did Not Work

Two clean negative results, both measured rather than argued.

Grid refinement does not improve the record constructions. Because a step function on n cells is also one on 2n cells, you can double the resolution of any witness for free and re-optimize with more freedom. It sounds like it should work. I tried it on both current record constructions with a trust-region sequential LP:

Witness	Cells	Descent per round	Gap to close
SimpleTES	2400 to 4800	1.2e-9	1.2e-5
Arena best	512 to 1024	8.6e-12	—

Both are already first-order stationary to within noise, and doubling the grid does not unlock anything. At those rates you would need thousands of LP solves to move the sixth decimal place. Local refinement is not the lever on this problem; better constructions come from better search, not finer grids.

The lower-bound architecture has a ceiling, and it is below the answer. I previously put that ceiling at 0.380713, and I have since withdrawn the derivation — its own per-row table produced a value above the certified upper bound, which a valid ceiling cannot do, and the published figure quietly substituted a min-over-rows quantity for the per-row one the argument actually bounds. What replaces it is weaker, and survives audit: by feasible-set containment, the discretised program is bounded by the continuum program at the same truncation parameters, and that limit is about 0.38065 at the parameters where the extremal function lives — pinned two independent ways. The upper bound is 0.3808591. So the architecture is short by roughly 2.1e-4 before any loss from the cover, and this line of attack cannot close the gap no matter how much compute it gets. Reaching mu needs a lower-bound architecture that does not factor through these duals, and I do not have one. Neither, as far as I can tell, does anyone.

What This Says About AI and Mathematics

The tempting version of this story is that agents caught an error in someone else's mathematics. That is not what happened. The published mathematics held up — White's paper is the thing the whole lower bound stands on, and re-reading it closely made my own work look worse, not his. What the agents caught was a reward-hacking artifact in an automated search pipeline, and the only reason it survived is that the pipeline's evaluator graded the number the program reported rather than the number the construction earns.

What the loop is genuinely good at is breadth under a fixed standard. Checking whether a cited number has a downloadable witness, fetching it, re-deriving it, and diffing against the claim is boring, mechanical, and exactly the kind of thing that does not get done — not because it is hard, but because nobody's incentive points at it. Running twenty of those in parallel found the normalization artifact in under fifteen minutes. Two independent agents then tried to refute the finding rather than confirm it, and one of them corrected the first's arithmetic — the ratio is 4096.9999999999/4096, not 4097/4096, and that last digit is what distinguishes a tuned constant from an off-by-one.

What the loop is bad at is knowing when its own output is a theorem. Every defect I found this round was in code an agent wrote and an agent reviewed, including the docstring that correctly described a safety margin and the implementation that never applied it. The model can state the right rigor standard and fail to meet it in the same file, with no internal signal that anything is wrong.

So the division of labor I would defend is narrower than the one I described last time. Agents for breadth, replication, and adversarial checking, where the standard is external and mechanical. Humans, or at minimum a genuinely independent tool like interval arithmetic, for deciding what counts as proved. The productive move this round was not asking an agent to be more careful. It was replacing a judgment call with a computation that cannot be talked out of its answer.

Where This Goes

The lower bound is written up as a preprint. What is left on it is not conceptual: the discretisation still has about 8e-5 of unrealised 1/N tail, though banking it now means redoing the region cover too, because three regions clear the binding value by under 3e-6 and would bind immediately. Given that a second group is working the same problem to the same standard, the interesting question is no longer whether the number can be nudged but whether it gets written down first.

If you want the full derivation — the certification argument, the twelve certificates, the upper-bound correction, and five approaches I ruled out with proofs — it is written up separately as a technical companion.

The upper bound side needs something I would rather see the community adopt than build alone. Every construction I have examined — three of three — fails an exact feasibility check by a microscopic amount, and none of the search systems producing them check their own arithmetic in anything but float64. That is how a bin count of n + 0.9999999999 survives into a paper. Exact certification of a 2400-cell witness takes about a second. There is no reason it should not be a required step, and I will run it for anyone who wants a construction checked.

A closing note on where the credit sits. The number in the headline is an increment on White's framework, and the increment is small next to the framework. If you read one thing from this post, read his paper instead.