The infimum is exactly D = 1.834430475762661711090753635125…, in a July 2026 manuscript of Darvas, Peng and Tao. Among monic polynomials with all roots in [−1,1], what is the infimum of the measure of the set where |f| < 1? Open since Erdős–Herzog–Piranian, 1958.
| field | as recorded at source |
|---|---|
| the claim | The infimum is exactly D = 1.834430475762661711090753635125…, in a July 2026 manuscript of Darvas, Peng and Tao. |
| the problem | Among monic polynomials with all roots in [−1,1], what is the infimum of the measure of the set where |f| < 1? Open since Erdős–Herzog–Piranian, 1958. |
| credited AI system | GPT-5.5 Pro (initial main argument in a solver–verifier framework, then revised by the human authors) |
| verification at source | Author-checked manuscript shipping its own three Arb certificates and two SymPy verifiers; the official Erdős-problems record was still open. |
| our verdict | CONFIRMED the computational fragment |
The extremal triple exists, is unique inside a certified box, lies in the admissible region, and every printed decimal of the extremal constants is correct — including all 30 claimed decimals of D.
This verifier prints one flat list rather than stages. All 22 named rows follow, in the order it emitted them.
| what the verifier proved | |
|---|---|
| 1 | (A.4) AD d/du F_R overlaps the printed closed form [AD -5.2402332, closed -5.2402332] |
| 2 | (A.5) AD d/dv F_L overlaps the printed closed form [AD 84.393443, closed 84.393443] |
| 3 | (A.6) AD d/du X_q(u) overlaps the printed closed form [AD -8.6686021, closed -8.6686021] |
| 4 | (A.12) 0 < p(q) < q < 1 uniformly on I_* [p in 0.824521729252520379285 .. 0.824521729252520379285] |
| 5 | (A.13) F_R(q, u0-1e-30) > 0 > F_R(q, u0+1e-30) on I_* (mean-value form) [F_R faces 0.00000000000000000000000000000405 .. 0.00000000000000000000000000000642 | -0.00000000000000000000000000000642 .. -0.00000000000000000000000000000405] |
| 6 | (A.14) F_L(q, v0-1e-30) < 0 < F_L(q, v0+1e-30) on I_* (mean-value form) [F_L faces -0.00000000000000000000000000009038 .. -0.00000000000000000000000000007839 | 0.00000000000000000000000000007839 .. 0.00000000000000000000000000009038] |
| 7 | Krawczyk (eqcert) proves existence + uniqueness of the triple [rounds 1, maxRad 3.84e-14] |
| 8 | B_* (A.9) is contained in the Krawczyk uniqueness box |
| 9 | high-precision Krawczyk image lands in the interior (existence re-proved) |
| 10 | refined enclosure width < 1e-40 in each coordinate [widths(quanta 1e-48): 1636, 3183, 1124] |
| 11 | q* inside I_* = q0 ± 1e-31 (A.11) — stronger than the B_* face |
| 12 | (q*,u*,v*) inside B_* = centres ± 1e-30 (A.9) => Lemma A.1 confirmed |
| 13 | claimed digits D (p.2, 30 dec) [rounded] |
| 14 | claimed digits alpha (p.5) [truncation] |
| 15 | claimed digits q* (p.24) [truncation] |
| 16 | claimed digits u* (p.24) [truncation] |
| 17 | claimed digits v* (p.24) [truncation] |
| 18 | claimed digits p* (p.24) [truncation] |
| 19 | claimed digits alpha (p.24) [truncation] |
| 20 | claimed digits r* (p.24) [truncation] |
| 21 | claimed digits z* (p.24) [truncation] |
| 22 | claimed digits D (p.24) [truncation] |
A verifier that cannot reject a false claim is not evidence, it is decoration. So each one carries mutation controls: the claim is deliberately corrupted and the verifier must refuse it. All 4 were rejected in the run that built this page, and a control that stopped firing would refuse the page instead.
| the corruption, and how it was caught | |
|---|---|
| 1 | M1 rejected: D last digit tampered (…125 -> …126) fails the digit check |
| 2 | M2 rejected: K with flipped sign has NO zero at the certified triple [F3_mut = 1.307440418726 .. 1.307440418726] |
| 3 | M3 rejected: box shifted by 1e-10 in q contains no zero of F_R [F_R over shifted box = 0.00000000118560 .. 0.00000000118560] |
| 4 | M4 rejected: p(q) constant 2 -> 2.000000001 breaks F_R at the triple [F_R_mut = -0.00000000047753 .. -0.00000000047753] |
The proof that this triple is extremal. We certified the number the manuscript names; we did not certify that no polynomial does better.
This is the part worth reading twice. The verdict at the top of this page is true inside its scope line and false outside it, and the sentence above is where the scope line comes from. Across all six claims in this set the same split appears: the computational fragment certifies and the analytic core does not — the flagship page measures exactly that.
git clone https://github.com/carlostoledo1891/cert-machine cd cert-machine node legacy/research/challenges/lane/laneb-lemniscate/verify.js
Plain Node, no packages. It prints the ledger above, runs its own falsifiers, and exits non-zero if anything fails. node instruments/laneaudit/audit.js runs all six.