Erdős–Herzog–Piranian asked in 1958 how small the set where a monic polynomial stays below 1 can be. Three separate AI-assisted full proofs of the answer are now claimed on the erdősproblems forum — and the forum states plainly that nobody associated with it has examined any part of them. This page adjudicates none of them. It reports what holds without them: a certified bracket, both ends unconditional.
| claim | who, when | AI used | examined by anyone? | checked here |
|---|---|---|---|---|
| inf = D exactly | Darvas, Peng, Runzhou Tao — 2026-07-15 | GPT-5.5 Pro (prover–verifier) | no | APPENDIX CONFIRMED |
| inf = D exactly | Shouqiao Wang | GPT-5.6 Sol | no | NOT AUDITED |
| inf = D exactly | Cristian Budala — 2026-08-24 | GPT-5.6 Sol | no | NOT AUDITED |
| inf ≥ 1.828 | this page | none — interval arithmetic | certified + independently re-verified | CERTIFIED |
| inf ≤ 1.8344304971959906 | this page | none — interval arithmetic | certified | CERTIFIED |
The forum's own words, on the page that lists all three: appearing there "is no guarantee of proof correctness, and does not mean that anyone associated with this site has examined any part of the proof." Three independent AI-assisted arguments agreeing on D = 1.83443047576266171109… is genuine evidence about the number. It is not a proof anyone has read.
To our knowledge no independent verification of any part of any of the three has been published — the forum says as much, and we would be glad to be shown otherwise. This repository has done one such check, and it is narrower than it sounds: we re-verified the computational appendix of the Darvas–Peng–Tao manuscript — the extremal triple exists, is unique in a certified box, and all thirty printed decimals of D are correct. That says nothing about the analytic core, which we did not audit and which is where a proof of this problem actually lives. It is, so far as we can establish, the only part of any of the three claims that anyone outside the authors has checked. The supremum side of the same problem is a separate program: the certified per-degree theorems on Tao's conjecture that sup = 2√2.
| end | value | how | cost |
|---|---|---|---|
| lower | ≥ 1.828 | pure forcing: a comb of unit-speed atoms and the finite-atom selector; no tail, no minimizer, no contradiction | 86 a₀-boxes / 1,350 b-boxes, 265 s |
| upper | ≤ 1.8344304971959906 | an explicit measure A·δ₋₁ + f dy on [a,1], its potential in closed form, the set structure from three one-line lemmas | seconds |
| the gap | 0.006430 | the price of demanding positivity on all of [0,1] rather than on the minimizer's own support — a different family, not a finer run | — |
The lower bound is the part worth reading twice. It does not assume a minimizer exists, does not argue by contradiction, and needs no tail estimate: for every normalized measure, either the component containing (−√2, 0) already reaches the bound, or a certified comb of atoms forces enough of the set into disjoint windows that the total length does. The whole analytic input beyond interval arithmetic is one Fubini identity, ∫Uνdμ = ∫Uμdν.
Honest limit of the method: the same forcing at the conjectured optimum can only push the moving atom as far as xR ≈ 0.0263, so the ceiling of this route is exactly the upper bound above — the method is exact in principle. The comb family in particular is exhausted near 1.828; its certified margin has already thinned to 4.12e-7, and finer boxes cannot buy the next thousandth.
In his notes on this problem Tao poses a model question (Problem 4.1): can the two-interval scenario be excluded for the explicit family λ(ε)? It is the crux obstruction on the way to the exact value. The answer certified here is yes, for every ε ∈ (0, 0.1] — 624,275 interval chunks cover [10⁻¹², 0.1] with a uniform certified margin, and a separate sliver lemma closes (0, 10⁻¹²] by an exact substitution that cancels the ε→0 singular pole algebraically rather than numerically.
The δ-mechanism, which is the interesting part. As ε → 0 the family's margin tends to a constant δ set by the level defect of the primal constants. With rounded constants δ can land on either side of zero, and if it lands negative the family provably fails below ε* ≈ 4.3·10⁻⁸. That was not predicted and then checked — the certifier found a decisively negative window first, and the mechanism was worked out afterwards to explain it. Anyone building small-ε duals from midpoint decimals will hit this wall; every construction posted on the thread sits far above it. The battery keeps the failure as a red control: flip the defect to the wrong side and the certificate must refuse.
Three dual measures posted in the thread carried the caveat that they had been checked by sampling. Sampling cannot decide positivity of a potential with poles. All three are certified here: every weight positive, and Uλ ≥ 0 on all of [−1,1] by adaptive tangent envelopes on each gap between support points — no quadrature, no grid. Certified off-atom minima: 1.243e-5 · 2.653e-6 · 3.959e-6.
It does not prove the infimum. It does not adjudicate any of the three claimed proofs — their analytic cores are outside what this instrument can reach, and pretending otherwise would be the exact failure this repository exists to avoid. It does not touch the supremum side. The bracket is what a machine can establish about this problem today without trusting anyone: a lower bound with a one-identity trust base, an upper bound from an explicit witness, and a named model problem closed for every ε. If any of the three claimed proofs is correct, the true value is D and this bracket contains it. The certificates and the instrument are public; every number above was recomputed at this build, and a REFUTED row or a missing fence refuses the page.