---

Claim. The answer is no: $f(z)=z^6-z$ is monic with six distinct roots, the six roots lie in six distinct connected components of the closed set $\{z:|f(z)|\le0.582\}$, and the component containing $0$ is not convex. These six are all the components of the set, because every component of $\{z:|f(z)|\le c\}$ contains a zero of $f$ (by the maximum modulus principle applied to $1/f$, with the open mapping theorem), a classical fact that the file does not prove. The Lean development Erdos1047 in Boris Alexeev's repository proves the statement about the roots as main_result and derives not_erdos_1047, which negates the file's own formal rendering of the problem (simple roots through roots.Nodup, components taken through the roots), a rendering that differs from the formal-conjectures statement added on 2026-08-04. The header of the posted file says that Aristotle, the system of Harmonic, found the proof given only the informal statement, and credits the original disproofs to Pommerenke, to Goodman and to Goodman's referee. The polynomial is the referee's $z(z^5-1)$ recorded in Goodman's paper, taken at a level just below the referee's critical value $5/6^{6/5}$ (an observation here, not the file's statement), so the proof is recorded as its own claim beside Pommerenke's accepted page and Goodman's page rather than as a formalization of either paper's argument.

Acceptance. Formalized. This corpus's verification built the repository's src/latest folder at the pinned commit 8822f7dd of 2026-09-15 (Lean v4.33.0, Mathlib v4.33.0). The built file is a later revision of the file posted on 2026-01-21 for Lean v4.24.0, also linked above: it states the same main_result and the same negation, with the header, the toolchain, the namespace and the proof scripts changed and the negation renamed not_erdos_1047 (the old name erdos_1047 remains as an alias), so the build certifies the revision, not the posted file. The axioms of Erdos1047.not_erdos_1047 are exactly propext, Classical.choice and Quot.sound, and its fingerprint was found identical to the comparator challenge ComparatorChallenges/ErdosProblems/Erdos1047.lean. The statement was audited clause by clause against the problem's Statement: every clause matches except one encoding, in which "the set has $m$ components" is rendered as "the $m$ roots lie in $m$ distinct components"; the two agree through the classical fact stated above, which no Lean file proves, so the disproof rests on that fact; requiring simple roots only strengthens the disproof. Not reviewed: the site's label, disproved with the Lean qualifier, refers to the development, but no reviewer of the proof independent of its author is named. Not refereed: the proof is published only as a Lean file in the author's repository.

Depends on. Nothing on the wiki; the development imports only Mathlib.