Erdős problem #852 asks how long a run of consecutive prime gaps can stay pairwise distinct. Its discussion thread conjectures h(x) ~ c0 · log x, held up by two constants produced by GPT models and published as bare decimals. This page replaces both with certified interval enclosures. One survives — as a rounding. The other is refuted at its 12th significant digit, and the wrong digits are not near the truth by accident: they are EXACTLY what an IEEE-754 double-precision product emits, because 87% of its factors round to 1.0 and silently vanish. The published constant is the bug, printed — the type specimen of a failure taxonomy this page names in §5, with a second specimen from the Ramanujan Machine's own sheets and a note in §6 for people who build evaluations on mathematical ground truth.
Local working document. The certified enclosures are theorems (every series truncated with an explicit remainder bound, every rounding directed outward, tail sums bounded by elementary integrals). The audits of the published decimals are exact-integer comparisons against those enclosures. One external identity is consumed for c0 — the dilog inversion formula (Lewin, Polylogarithms, eq. 1.12) — and one elementary-calculus fact, I0'(c) = log((e^{2c}−1)/2c); both are independently cross-checked in the battery.
| constant | the thread says | certified value | method | verdict |
|---|---|---|---|---|
| c0 | 1.32322827686395… | 1.323228276863949469… | root of I0(c) = 1 · 200 certified bisections | VERIFIED (as a rounding) |
| C* | 0.0752403861777… | 0.075240386178309… | Euler product over 1,857,858 odd primes + proved tail | REFUTED at digit 12 |
Transcribed from the pinned bytes of the problem page and discussion thread (erdosproblems.com/852, fetched 2026-08-25; sha256 re-hashed during this build — a drifted source refuses the audit). Both values were published by DavidTurturean on 2026-04-24, produced via GPT-5.5 Pro; the thread's conjectured asymptotic h(x) ~ 1.32323 · log x rests on c0, and the conditional lower-bound argument ruling out h(x) = o(log x) rests on the combined rate (1/2 + C*)c² + O(c³).
C* = (1/2)(∏_{p≥3}(1 + 1/(p−1)³) − 1). In IEEE-754 double precision, 1 + 1/(p−1)³ rounds to exactly 1.0 as soon as 1/(p−1)³ < 2⁻⁵³ — that is, for every prime p beyond ≈ 208,000. A naive float loop over any prime limit therefore computes the product only to p ≈ 2·10⁵ and silently discards everything after; the discarded mass is Σ_{p>208064} 1/(p−1)³ ≈ 9.1·10⁻¹³ of log-product — which is precisely the size of the error in the published digits. Re-measured live during this build, over the odd primes to 2·10⁶:
| computation | result | status |
|---|---|---|
| naive double product (drops 87.5% of factors) | 0.0752403861777419 | = the published value, digit for digit |
| double log1p sum (keeps every factor) | 0.0752403861782102 | float-honest, still uncertified |
| certified enclosure at the same limit | [0.0752403861783044, 0.0752403861783764] | the authority |
The published 0.0752403861777418 matches the naive float product to every printed digit and lies provably BELOW the certified enclosure. The constant was not approximately right with unlucky digits — it is the float artifact itself, published with 13 digits of confidence when only 11 were real. No amount of raising the prime limit would have fixed it; the loop was already ignoring every prime past 2·10⁵. This is the impostor-catalog failure mode inverted: there, true constants impersonate closed forms past every float screen; here, a float screen impersonated a constant.
c0 is the unique positive root of I0(c) = 1, where the rate function of the iid geometric-gap model is
The dilog argument 1 − e^{2c} ≈ −13.1 sits far outside the series disk, so the certificate routes through the inversion identity Li2(−x) = −π²/6 − (1/2)log²x − Li2(−1/x), leaving only Li2 at −1/x ≈ −0.076, where the defining series converges with a geometric tail bound. Everything else is exp, log and π at 320-bit directed rounding. The root is then bisected 200 times, each step a certified strict inequality I0(m) < 1 or I0(m) > 1. Uniqueness is free: the derivative collapses to
and the strict inequality e^{2c} > 1 + 2c is itself certified on the bracket. The certified value:
The thread's printed 1.32322827686395… is a correct ROUNDING to 14 places — but its trailing ellipsis is a half-ulp slip: the true expansion continues …9469, not …95. Harmless here, but exactly the kind of slip a truncated-decimal culture cannot see, and an enclosure culture cannot miss.
Doubles cannot certify C* (they cannot even compute it, §2), and exact rationals cannot afford it — the exact partial product over primes to 3·10⁷ has a denominator of ~10⁷ digits. The instrument built for this report (instruments/bigfloat/) is the missing middle: BigInt mantissa · 2^e with DIRECTED rounding, so every partial product is an interval [lo, hi] that provably brackets the exact rational product at 192 bits. The infinite tail is a certified multiplier:
using only p ≥ L+1 ⇒ p−1 ≥ L. At L = 3·10⁷ the tail is ≤ 5.6·10⁻¹⁶ and the whole enclosure is 3.20e-16 wide. The same product engine is calibrated in the battery against a case with a known answer — ∏_{p≥3}(1 + 1/(p²−1)) = π²/8 (Euler) — and the tail check has a mutation red control: zero the tail bound and the calibration enclosure must EXCLUDE π²/8. It does. A tail that cannot be missed is not being checked.
C* is not an anecdote; it is the TYPE SPECIMEN of a failure class, and this machine's records now hold three distinct classes, each certified, each with the detector that catches it. They are worth naming because the usual defenses — rerun it, cross-check digits, add compute — catch none of them.
| class | specimen | why digit-checking cannot catch it | what caught it |
|---|---|---|---|
| 1 · The artifact published as truth. The computation is silently wrong; its output is stable. | C* (this page): 87% of factors round to 1.0; 13 digits printed, 11 real | Every naive rerun reproduces the SAME wrong digits — two independent float implementations agree with each other, not with the truth. More compute changes nothing: the loop already ignores every prime past 2·10⁵, so raising the limit reads as convergence. | An exact arbiter: a certified enclosure the published value provably lies outside. |
| 2 · The true computation under a false printed claim. The numerics were right; the published identity is not what they computed. | Ramanujan Machine, mixed-zeta sheet row 3: printed 2/(2ζ(5)−2ζ(3)−1) ≈ -1.5035; the row's own polynomials converge to 2.98622586… = 2/(2ζ(5)−2ζ(3)+1) — a sign slip | The mismatch is between a formula and a table, not between two numbers — there is no second number to check digits against. The sheet's displayed convergent (a₁ = 275 vs the polynomial's 75) was itself wrong. | Deciding the printed identity against a certified CF enclosure: disjoint, REFUTED — and the corrected identity certified on the SAME enclosure, so the mechanism is proved, not guessed. |
| 3 · The coincidence that survives every screen. Nothing computed wrong; the world just contains near-misses deeper than any float. | The impostor catalog: a published OEIS constant impersonates 1/5 for 62 significant digits | 62 digits of agreement passes any decimal screen ever used to announce a discovery. Probability arguments certify confidence, not truth. | Exact BigInt refutation at full published precision — the only test with a zero false-accept rate. |
Class 2 is re-certified live during this build (the printed row must come out REJECT with the sign-slip mechanism, the correction HIT, or this page refuses to render); the full 52-row registry is the companion report. Class 3 has its own catalog. What the three classes share: the failure is invisible from inside floating point, stable under repetition, and wears the costume of precision.
The C* episode is what the default researcher-plus-model workflow produces: a competent person, a frontier model, a serious venue, a constant stated to 13 digits with no error bound — wrong at digit 12 in a way no rerun would reveal. Three consequences for anyone building evaluations or verifiable-reward environments on mathematical ground truth:
The constructive direction: ground truth as certificates (exact rationals, directed-rounding enclosures, detached verifiers in stdlib Python with zero code shared with the generator) makes "the model was right" a theorem rather than a grade — false positives provably false. This repository's audit corpus and instruments are built as exactly that substrate.
make test re-runs all of it: the bigfloat layer against exact rationals on random operands with π, ln 2 and e certified to 50 literature digits (14 checks, 5 red controls), and the erdos852 battery (22 checks, 5 red controls) — the π²/8 calibration with its mutation red, the derivative identity, the dilog inversion against direct quadrature, the bracket re-certification, the forged-pin refusal, and the naive-float reproduction of the published digits, live, every run. This page itself refuses to build if any verdict, digit, or the mechanism reproduction moves.
Everything above runs on this project's own stack — and a fair objection is that the stack and the claims share an author. So the refutation also ships as a Lean 4 artifact (lean/erdos852/ in the repository): the odd primes up to 400,000 as data, a ten-line trial-division certifier with a machine-checked correctness theorem against Mathlib's Nat.Prime, and the ONE integer inequality — the exact partial product N/D over those primes satisfies 5·(N−D)·10¹² > 752403861778·D, i.e. (N/D−1)/2 already exceeds the upper edge of the published claim's window. Every ingredient is re-proved by the Lean kernel: primality of all 33,859 listed primes, strict ascent (no prime counted twice), oddness, and the inequality itself.
The prime list needs no trust at all: an omitted prime only WEAKENS the lower bound, and every other defect — a composite, a duplicate, an even entry, an inflated claim — makes the build fail, which is exactly what lean/erdos852/check.sh demonstrates: three deliberately forged variants must be REJECTED by the kernel before the green build counts.
The full-scale run is the demonstrated state: all 33,859 primes certified through the kernel (240 modules), the ascent and oddness checks green, and two spec theorems (N_spec, D_spec) proving — by pure rewriting, no arithmetic — that the tree of chunk subproducts the kernel evaluates IS the product over the full prime list. The forged variants (a planted composite, a broken ascent, an inflated claim) are rejected by the same kernel, every check.sh run.
What stays outside Lean, stated plainly: the one-paragraph argument that a partial product of factors > 1 over a subset of the primes lower-bounds the full convergent product, and the transcription of the published constant. The kernel replaces this project's BigInt arithmetic, not the definition of C*.