On 16 December 2025 Tao reformulated Erdős #1038 over discrete probability measures, asked for the supremum of |{U_μ < 0}|, and conjectured 2√2 — “this may be hard to prove completely.” Within the week the problem's forum had a proof, written up by Tao with its equality case. For rational weights the question is about root-constrained polynomials, decidable degree by degree; this machine re-decided degrees 3 to 8 in exact arithmetic, sharing no idea and no code with the proof: the odd ones stay below 2.82, and the even ones are placed in [2√2, 2.82845]. Re-decisions of a known theorem, not progress on it.
A known theorem, re-decided. That |{U_μ < 0}| ≤ 2√2 for every probability measure on [−1,1], with the two-atom measure the only case of equality, is Theorem 2.1 of Tao's notes of December 2025; erdosproblems.com/1038 records sup = 2√2 and google-deepmind/formal-conjectures marks erdos_1038.parts.ii “research solved”. The per-degree certificates below neither use nor replace it. Until 2026-10-05 this page called the supremum an open conjecture; that was wrong. Every number on this page is a certified outward enclosure recomputed at this build; nothing is decided in floating point. Not peer-reviewed.
Erdős #1038 asks how small, and how large, the sublevel set of a polynomial with constrained roots can be. Its infimum side is still open on the problem page: three AI-assisted proof claims of 2026 report the same constant, none examined by the site, and this lab independently verified the computational fragment of one of them (Darvas–Peng–Tao) and brackets the infimum unconditionally. In erdosproblems#179 (16 December 2025), Tao posed the other end: over discrete probability measures μ = Σ pᵢ δ_{aᵢ} on [−1,1], with logarithmic potential U_μ(x) = Σ pᵢ log|x − aᵢ|, how LARGE can |{x : U_μ(x) < 0}| be?
His conjecture: the supremum is 2√2, attained by the uniform measure on {−1, +1} — and “this may be hard to prove completely.” It was proved within the week, in the problem's forum thread: on 21 December 2025 Tao posted a write-up completing the proof (AlphaEvolve proposed the weights for one regime), two participants confirmed it the same day, and his notes (27 December 2025, Theorem 2.1) state it with its equality case: L(μ) ≥ 2√2 forces μ = ½δ₋₁ + ½δ₁. The problem page records sup = 2√2; formal-conjectures marks erdos_1038.parts.ii “research solved”, proved in Tao's notes. This campaign (2026-09-01) was framed on the GitHub issue, which had no replies; the forum's resolution predates it.
So the theorem, restricted to rational weights of denominator N, is a statement about degree-N polynomials — a finite-dimensional object that exact arithmetic can decide degree by degree, without the potential theory. That is what this page re-decides: a second route to statements already known, not a new one.
The boundary of {|q| < 1} consists of roots of the integer polynomials A ∓ dᴺ (A the root-scaled form of q). Those are isolated and refined by the BigInt Sturm machinery of the trigmin instrument — the code calibrated on Mercer's closed forms in the λ(4) campaign — and each gap between boundary roots is decided by one exact rational comparison. The measure is summed outward: a true enclosure, never a float.
| polynomial | certified measure of {|q|<1} | exact value |
|---|---|---|
| x² − 1 | [2.828427124746, 2.828427124747] | 2√2 = 2.8284271247… |
| x² | [1.999999999999, 2.000000000000] | 2 |
| x | [2.000000000000, 2.000000000001] | 2 |
| (x−1)² | [2.000000000000, 2.000000000001] | 2 |
| (x²−1)² | [2.828427124745, 2.828427124746] | 2√2 again — even powers of the witness keep it |
The last row is why even degrees are different: powers of the witness keep its measure, so (x²−1)^{N/2} attains 2√2 at every even degree, and no even degree can fall strictly below 2√2 the way the odd ones do.
| degree | certified statement | boxes | depth | time | |
|---|---|---|---|---|---|
| N = 3 | every degree-3 polynomial stays below 2.82 < 2√2 — an explicit margin under the supremum | 127 | 16 | 0.0 s | strict |
| N = 4 | the degree supremum lies in [2√2, 2.82845]; (x²−1)^2 attains the left end (the theorem gives exactly 2√2) | 549 | 59 | 0.1 s | localized |
| N = 5 | every degree-5 polynomial stays below 2.82 < 2√2 — an explicit margin under the supremum | 1,583 | 37 | 0.2 s | strict |
| N = 6 | the degree supremum lies in [2√2, 2.82845]; (x²−1)^3 attains the left end (the theorem gives exactly 2√2) | 4,219 | 89 | 0.6 s | localized |
| N = 7 | every degree-7 polynomial stays below 2.82 < 2√2 — an explicit margin under the supremum | 28,773 | 63 | 8.8 s | strict |
| N = 8 | the degree supremum lies in [2√2, 2.82845]; (x²−1)^4 attains the left end (the theorem gives exactly 2√2) | 31,425 | 118 | 5.7 s | localized |
Each row quantifies over EVERY root configuration in [−1,1]ᴺ — collisions and multiplicities included — through the ordered-and-mirrored branch-and-bound: a box is closed when the certified measure of {Π dist(x, Iᵢ) < 1} falls below the threshold, and that bound equals the true measure on thin boxes (a battery check). In measure language: every discrete probability measure on [−1,1] whose weights have denominator 3, 5 or 7 satisfies |{U_μ < 0}| < 2.82; for denominators 4, 6 and 8, the certified upper end is within 2.3×10⁻⁵ of 2√2 — weaker than Tao's theorem, which gives exactly 2√2 there, reached by an unrelated route.
deg9: bnb: box budget exhausted — recorded as attempted and refused, not silently dropped. Its answer is known from the theorem; the refusal is the instrument's budget, not an open question.