Open on the site: the label is OPEN (page last edited 29 December 2025; no proof claim on its tab). The standing derived from the claim pages is solved, claim proved: Theorem 1.1 of the OpenAI mathematics release's manuscript of 25 September 2026 gives $N(b)\le c_2\log\log b$ for every $b\ge b_0$, so $N(b)\ll\log\log b$ and, with Erdős's lower bound of 1950, $N(b)\asymp\log\log b$. The claim is accepted on formalized evidence alone, the Lean declarations the corpus's verification built and audited, as its claim page (OpenAI, 2026) records; it has no outside review and no refereed publication. The earlier bounds have accepted partial claim pages on their refereed papers: Erdős's 1950 bounds $\log\log b\ll N(b)\ll\log b/\log\log b$, and Vose's 1985 bound $N(b)\ll\sqrt{\log b}$, which replaced Erdős's upper bound. Two pending partial claims do not change the standing: van Doorn and GPT-6 Astra Pro's squared double-logarithm bound of 16 September 2026, implied by the accepted bound, and a Lean proof by Harmonic's Aristotle prover of the lower bound $\log\log b\le6N(b)$, published in 2026 and not built here. The conjecture $N(b)\ll\log\log b$ was stated by Erdős in 1950 and repeated in the 1980 monograph.