---

Claim. Let $R_n$ be the infimum of $\rho(p)$ over monic polynomials $p$ of degree $n$ with all zeros in the closed unit disk, where $\rho(p)$ is the inradius of $\{z:\lvert p(z)\rvert<1\}$ as in Problem 1039. Then

$$nR_n\to\frac{\pi}{2},$$

so $R_n=(\pi/2+o(1))/n$, with $p(z)=z^n-1$ supplying the matching upper bound that Erdős, Herzog and Piranian noted. The preprint From $\log2$ to $\pi/2$: the sharp asymptotic inradius of polynomial lemniscates by Yujian Geng and Dong Qiu appeared on arXiv on 2026-09-06, and the claim was registered on the site's proof-claims tab on 2026-09-09 by the user JPkkk, with ChatGPT named as assisting in the proof development, including the reflection identity, and in the Lean formalization. The route: the exact universal radius $2^{1/n}-1$ for disks centered at zeros recovers the $(\log2)/n$ bound of [[problems/polynomials/E1039/claims/2026_05_07_price|Price 2026]]; starting from the matched-product inequality that the site's curator stated on the thread, the authors show that a polynomial with a small inradius must have its zeros concentrated near one radius, with the low negative moments of the zeros decaying; after rescaling, such polynomials converge to an entire function whose modulus obeys a reflection identity; a further rescaling and the three-lines theorem show that the limiting set where this function has modulus below $1$ contains disks of every radius smaller than $\pi/2$; and carrying these disks back to the polynomial gives the lower bound. The authors state that the main theorem and its supporting formal proof are verified in Lean 4, rechecked with the Canto Prover, in a companion repository frozen on 2026-09-06, whose README says the build checks $nR_n\to\pi/2$ and does not claim the bound $R_n\ge\pi/(2n)$ for every $n$.

Submission note. Posted to erdosproblems.com as a proof claim by Yujian Geng and Dong Qiu (account JPkkk) on 9 September 2026, giving "ChatGPT" as the AI used:

We prove that $R_n=(\pi/2+o(1))/n$, where $R_n$ is the infimum of $\rho(p)$ over the polynomials in this problem. Building on Bloom’s matched-product inequality, we show that small inradius forces radial concentration of the zeros and decay of reciprocal moments. This yields an entire scaling limit with a modulus reflection identity. A second rescaling and three-lines convexity produce disks of every radius below $\pi/2$ in the limiting sublevel set. Transferring these disks back gives the lower bound; $p(z)=z^n-1$ supplies the matching upper bound. Notes: This work was inspired by Bloom’s post. ChatGPT assisted with proof development, including the reflection identity, and Lean formalization. The formal proof was subsequently rechecked using Canto Prover. Detailed contributions and acknowledgments to earlier contributors are given in the paper.

Depends on. No page of this wiki. The lower-bound argument starts from the matched-product inequality that the site's curator stated on the thread, recorded on Price 2026, but the preprint proves it itself as Proposition 2.3 of its Section 2, with credit to Price, Sothanaphan, Bloom and Kitamura; the link is lineage, not a dependency.

Standing. Claimed. The claim has no comments on the tab, the site labels the problem OPEN (page last edited 27 December 2025), the preprint is not refereed, and the Lean development was neither built nor audited here. The problem's first question, to determine the behavior of $\rho(f)$, is read as its source states it, the asymptotic behavior of the minimal inradius $\rho_n=R_n$ (the problem page's Formulation); this claim would settle it with the sharp constant, and with it the second question, whether $\rho_n\gg1/n$.