Why a proved theorem still needs reproducible claim custody
On May 20, 2026, OpenAI announced that an internal reasoning model had produced a counterexample to the Erdős planar unit-distance conjecture.
The problem is easy to state: given $n$ points in the plane, how many pairs of points can be exactly distance $1$ apart?
For nearly eighty years, the prevailing expectation was that square-grid-type constructions were essentially optimal up to a slowly growing exponent. OpenAI’s announcement changed that. Its internal reasoning model produced an infinite family of examples giving a polynomial improvement, and the proof was checked and written up in mathematical form by external mathematicians.
In this article, “the remarks paper” refers to the companion PDF by Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, and Matchett Wood, linked from OpenAI’s announcement.
The proof-level result belongs to those authors and the source papers.
My focus here is narrower: equation (2.2) in that remarks paper, and whether its explicit numerical value can be reproduced as executable code.
This is not about proving the theorem again. It is about what happens after a theorem contains a fragile numerical claim.
The proof is not the artifact
A mathematical proof and a software artifact do different jobs.
The proof establishes the theorem. It gives the definitions, the argument, the dependencies, and the mathematical reason why the result holds.
A software artifact should not pretend to replace that.
But some claims inside a mathematical paper have a finite, numerical, or computationally checkable surface. Those claims can be preserved differently. They can be run. They can be tested. They can fail when precision is wrong.
That is the narrow role of an executable reproduction artifact: not proof replacement, not automated peer review, and not authority over the theorem, but a reproducible object for the part of the claim that can be computed.
The specific target: equation (2.2)
In the OpenAI Erdős result, one checkable surface is equation (2.2) of the remarks paper.
For the explicit choice
the remarks paper gives an explicit numerical lower bound on the exponent excess above the classical Erdős exponent:
These parameters are taken directly from the remarks paper without modification. The artifact does not derive the multiquadratic choice; it reproduces the finite numerical calculation built from that choice.
This is not the later stronger explicit bound associated with Sawin’s separate preprint. It is not $\delta \approx 0.014$. It is the numerical value appearing in equation (2.2) of the remarks paper.
That narrowness is important. It is exactly what makes the claim suitable for executable reproduction.
Where the numerical fragility comes from
The numerical fragility comes from the exact form of equation (2.2), not from a large computation.
Immediately after the published expression, the parameters are:
and
With the paper’s definitions of $u, v$, and $\delta$ substituted into equation (2.2), the exponent excess reduces to:
The constant $36$ is not introduced by the implementation. It is already present in the remarks paper’s equation (2.2), both in the numerator term $u\pi/(36v)$ and in the denominator term $\log(36/\delta^2).$
After substituting $u = K/r^2, v = r/2$, and $\delta = 101^{-2K}$, the numerator simplifies to $\log(K\pi / 18r^3)$, while the denominator becomes $\log 36 + 4K \log 101$.
Here the $101$ comes from the finite prime in $S = {101, \infty}$.
In other words, this artifact does not derive the constant $36$ from first principles; it reproduces the published equation with the stated substitutions.
The precision problem is in the numerator:
Because $K$ is the ceiling of $18r^3 / \pi$, the ratio $K\pi / 18r^3$ is only barely larger than $1$.
More precisely:
For $r = 510510$,
So the numerator is effectively $\log(1 + \varepsilon)$ with $\varepsilon$ at the $10^{-18}$scale.
IEEE 754 double precision has machine epsilon around $2.2 \times 10^{-16}$. A naive float64 computation therefore cannot reliably distinguish the near-one ratio from $1$. The ratio rounds to $1$, leading to $\log(1) = 0.$
The exponent excess disappears before the computation reaches the value stated in the paper.
This is not a flaw in the mathematics. It is a precision failure in the numerical evaluation of a valid expression. That is the reason the artifact evaluates equation (2.2) using mpmath at 200-bit precision.
A PDF can state the value. A verifier can expose when the value disappears.
What we built
We built:
https://github.com/Flamehaven-Labs/openai-erdos-eq22-reproduction
The purpose is deliberately narrow: reproduce the finite, explicitly checkable numerical surface of equation (2.2) in the OpenAI Erdős unit-distance disproof remarks.
The package evaluates the expression using mpmath at 200-bit precision and returns:
6.2391e-38
This matches the published two-significant-figure value $\approx 6.24 \times 10^{-38}$ to $1.4 \times 10^{-4}$ relative error.
The repository includes 60 unit tests, 21 verifier checks, a frozen per-source-file SHA-256 manifest, GitHub Actions CI across Ubuntu and Windows, Python 3.11 / 3.12 verification, and a frozen-report mode that prints a verdict without mutating tracked evidence.
The basic reproduction path is:
git clone <https://github.com/Flamehaven-Labs/openai-erdos-eq22-reproduction>
cd openai-erdos-eq22-reproduction
pip install -e ".[dev]"
python -m erdos_ant.verify
Expected output includes:
Verdict: PASS
Checks: 21/21 passed
eq (2.2) exponent excess: 6.2391e-38
This is not a large system. That is part of the point. A small claim with a clear boundary is easier to inspect than a broad claim that blurs proof, computation, and interpretation.
From reproduction to custody
This repository was not built as a one-off reaction to an OpenAI announcement. We are not announcing a grand framework here; we are showing the discipline in miniature.
For us, the work is part of a longer routine: take a mathematical or technical claim, isolate the checkable surface, pin the environment, and make drift visible.
That is intentionally plain work.
Read the source.
Extract the claim.
Reproduce the computation.
Record the boundary.
Let the verifier fail if the result disappears.
To execute this routine reliably, the scope must be uncomfortably narrow. This repository intentionally leaves the proof of Theorem 1.1, the construction of the infinite tower, and Sawin’s separate $\delta \approx 0.014$ preprint to their respective sources. It does not pretend to be peer review.
This is not just a disclaimer. It is the point of the artifact.
A sharp, restricted boundary is exactly what makes a claim inspectable, repeatable, and challengeable. This is what I mean here by claim custody.
It addresses a technical governance question, but not in the policy sense: what exactly is being trusted, from which source, and what makes the claim fail if the implementation changes?
A PDF can state the value. A verifier can expose when the value disappears.
We claim no authority over the broader theorem. We simply maintain a reproducible boundary around the fragile numerical claim inside it.
Closing
The theorem was proved in the mathematical papers.
This repository asks a smaller question: can the numerical value in equation (2.2) survive execution?
In float64, it does not. The exponent excess collapses to zero.
At 200-bit precision, with the source parameters pinned and the verifier running under CI, the artifact recovers:
6.2391e-38
matching the published value to $1.4 \times 10^{-4}$ relative error.
That is the point.
Not a new theorem. Not a proof replacement.
A reproducible claim surface for one precision-sensitive number in a major AI-assisted mathematical result.
Repository:
https://github.com/Flamehaven-Labs/openai-erdos-eq22-reproduction
Paper / Zenodo: