---

Claim. For every monic $f(z)=\prod_{i\le n}(z-z_i)$ with $\lvert z_i\rvert\le1$, some root $z_j$ is the center of a disk of radius $(\log2)/n$ contained in $\{z:\lvert f(z)\rvert<1\}$, so $\rho(f)\ge(\log2)/n$; with $f(z)=z^n-1$, whose inradius is at most $(\pi/2)/n$, this gives $\inf_{\deg f=n}\rho(f)=\Theta(1/n)$ and answers the second question of Problem 1039 in the affirmative. The argument, posted on the site's discussion thread on 2026-05-07 by Liam Price with GPT-5.5 Pro named as the system used, is a product estimate: if no such disk exists, there are points $w_j$ with $\lvert f(w_j)\rvert\ge1$ and $\lvert w_j-z_j\rvert<c/n$ for some $c<\log2$, and the double product $\prod_j\prod_i\lvert w_j-z_i\rvert$, which is at least $1$, is at most $(e^c-1)^n<1$. The constant $\log2$ is sharp for disks centered at roots, as $z^n-1$ shows. Nat Sothanaphan posted a streamlined account on 2026-05-08 (notes), and the site's curator, Thomas Bloom, stated on 2026-05-11 the inequality $\prod_j\lvert f(w_j)\rvert\le((1+\epsilon)^n-1)^n$ whenever $\lvert z_i-w_i\rvert\le\epsilon$ for all $i$, from which the bound follows, asking whether it is new and for a Lean proof of it. Kenta Kitamura's Lean 4 development of 2026-05-15, based on Price's write-up and the thread, formalizes the argument, with assistance from Codex 5.5 disclosed.

Covers. The lower bound $\rho_n\ge(\log2)/n$ for the minimal inradius $\rho_n=\inf_{\deg f=n}\rho(f)$, hence, with $z^n-1$, the exact order $\rho_n=\Theta(1/n)$ and a yes to the second question. Read as its source states it (the problem page's Formulation), the first question asks for the asymptotic behavior of $\rho_n$; this claim gives its order and not the sharp constant $\lim n\rho_n$, which is the later full claim on Geng–Qiu 2026.

Depends on. No page of this wiki.

Standing. Claimed. Sothanaphan wrote on the thread that they had digested the argument and could vouch for its correctness (2026-05-08) and, after Kitamura's formalization, that an AI check confirmed it (2026-05-17); Bloom wrote that Bloom was sure the proof in the note was fine while asking for a formal proof of the inequality. The site labels the problem OPEN (page last edited 27 December 2025, before these postings), no proof claim was registered on the site's proof-claims tab, no refereed or arXiv version of the note exists, and the Lean development was neither built nor audited here; the corpus records the endorsements and does not read them as the site's acceptance. The argument is reproduced, with credit to Price, Sothanaphan, Bloom and Kitamura, as Section 2 of the Geng–Qiu preprint.