---

Claim. The answer is no: with $r=2^{1/10}$, so $0<r<2$, the monic polynomial $f(z)=z^{10}-2$ has all its roots on $|z|=r$, and every connected component of $S=\{z:|f(z)|<1\}$ has diameter at most $0.2$, below $2-r\approx0.93$. The Lean file Erdos1048b in Boris Alexeev's repository proves this: the components of $S$ are the images of the unit disc under the ten branches $g_k(w)=\zeta^k(w+2)^{1/10}$ of the inverse, each image of diameter at most $2/10$ (my_g_diam), and the final theorem bounds the diameter of the component of every point of $S$ strictly by $2-r$; it is components_small_final in the posted file and erdos_1048 in the later revision, which keeps the old name as an alias. The author's thread post of 2026-01-28 says that Aristotle, the system of Harmonic, found the proof from the problem statement alone and chose the polynomial itself; the posted file names no source, and the later revision lists Aristotle as its informal author and Aristotle and Boris Alexeev as its formal authors. The example is a member of Pommerenke's family $z^n-r^n$ with $n=10$ and $r^{10}=2$ (an observation here, not the file's), so it is recorded as its own claim beside Pommerenke's accepted page, which carries the author's separate formalization of the paper's example.

Acceptance. Formalized. This corpus's verification built Boris Alexeev's repository at the pinned commit 8822f7dd of 2026-09-15, in its src/latest project (Lean v4.33.0, Mathlib v4.33.0): the module ErdosProblems.Erdos1048b compiled with no sorry and no declared axiom, beside its comparator challenge Erdos1048b. The built file is a later revision of the posted Lean 4.24.0 file, which the thread post links to an online type-check: it is ported to the newer toolchain, its proofs are reformatted and its final theorem is renamed, so the build certifies that revision and not the posted file. The axioms of Erdos1048b.erdos_1048 are exactly propext, Classical.choice and Quot.sound. The challenge pins that theorem with the definitions my_r, my_f and my_S of $r$, $f$ and $S$, and the fingerprints of the theorem and of the three definitions were found identical to the challenge. The statement was audited clause by clause against the problem's Statement: erdos_1048 says that for every $z\in S$ the connected component of $z$ in $S$ has diameter below $2-r$, and together with my_f_monic, my_f_nonconstant, roots_in_disk and my_r_lt_two from the same module it carries this page's claim exactly, a disproof for $r=2^{1/10}>1$, away from the degenerate case $r=0$. Those four facts lie outside the compared statement; they are proved in the compiled module and each is elementary. The repository's formalization of Pommerenke's example, Erdos1048, is a different result and belongs to Pommerenke's page. Not reviewed: the site's label DISPROVED (LEAN) and the formal_proof attribute of the formal-conjectures statement file refer to that other formalization, and no outside reviewer of this proof is named. Not refereed: the proof is published only in the repository and the thread post.

Depends on. Nothing on the wiki.