Erdős #1038: every printed decimal of the extremal constant is right — and the famous 30th digit is a rounding, not an expansion

The Darvas–Peng–Tao manuscript solving Erdős Problem #1038 (Erdős–Herzog–Piranian 1958) prints the extremal value D = 1.834430475762661711090753635125… to 30 decimals, defined implicitly by a 3-dimensional nonlinear system, and ships its own Arb and SymPy certificates. We rebuilt the computational fragment as an independent reimplementation — one shared definition of the system over two of our own interval backends, automatic differentiation for the Jacobian, Krawczyk for existence and uniqueness — and it holds: 26 checks, 4/4 mutation controls rejected, under 0.1 s, with certified enclosures to 40+ decimals. Along the way the machinery surfaced two things worth publishing: the headline value’s last digit is a half-up rounding presented with an expansion’s trailing “…”, and one of the paper’s face inequalities is uncertifiable by naive interval evaluation at the printed radii — it needs (and gets) a first-order mean-value form.

The two findings

1. The 30th decimal. The manuscript’s p.24 constants — q*, u*, v*, p*, α, r*, z*, and D to 18–19 decimals — all match our certified enclosures as exact truncations of the expansion. The headline D on p.2, printed to 30 decimals ending “…635125…”, does not: the true expansion continues …6351247861…, so the 30th decimal of the expansion is 4, not 5. The printed value is a correct half-up rounding, accurate to under 5×10⁻³¹ — but the trailing ellipsis conventionally promises an expansion prefix, and read that way its last digit is off by one. Not an error in the mathematics; a presentation defect the digit machinery caught, and the reason mutation M1 (tamper that digit to …126) is rejected in both directions.

2. Inequality (A.13) resists naive intervals. The face inequality sits about 5×10⁻³⁰ from zero, while naive interval evaluation over the printed box inflates the width to about 1.2×10⁻²⁹ — the quotient p(q) alone evaluates ~14× wider than its true derivative — so the sign is naively indeterminate at the printed radii. Our proof of (A.12)–(A.14) uses the rigorous first-order mean-value form F(m) + J(box)·(box−m) with the AD Jacobian. (No claim is made about the authors’ own Arb run, which we did not execute.)

What was verified

The manuscript defines D implicitly: (q*,u*,v*) is the zero of a 3-dimensional system built from Λ(y) = log((1+y)/(1−y)) inside the box B* = (q₀,u₀,v₀) ± 10⁻³⁰; then D = r* − z*. One shared implementation of the system, written over an abstract arithmetic backend with forward-mode AD jets, runs over two backends: eqcert’s outward-rounded double intervals, and a fixed-point BigInt interval layer with 10⁻⁴⁸ quantum and directed rounding (log by atanh series with an explicit tail bound). The AD partials agree with the manuscript’s displayed closed forms — two independent routes to the same derivatives. Krawczyk proves existence and local uniqueness (contraction on the first round), B* sits inside the uniqueness box — so the manuscript’s triple and ours are the same zero, confirming its Lemma A.1 — and iterating K in the high-precision layer refines the enclosure below 3.2×10⁻⁴⁵ per coordinate, enough to check every printed digit with 15 decimals to spare.

What was NOT audited, stated so it cannot be assumed

Why a solved problem was worth re-checking

This claim already carries author-side Arb certificates — the strongest evidence class in the database. What an independent reimplementation adds is exactly what it added here: enclosures a stranger can regenerate in a tenth of a second, one presentation defect at the headline digit that only a certified expansion could adjudicate, and a documented case where the printed verification radii are too coarse for the naive method a reader would first try. Confirmation plus sharpened fine print is what the lane is for.