---

Claim. There is a monic polynomial $f$ of degree seven with all roots in the open unit disk such that no path of length less than $2$ inside $\{z:\lvert f(z)\rvert<1\}$ connects two of its roots, so the answer to Problem 1041 is no. The user ani posted the write-up on the site's discussion thread on 2026-09-07, with GPT 6 named as the system used, describing a family of polynomials depending on a small parameter $s$ in which the lemniscate component holding two roots has a bottleneck at a critical point, so that any connecting path must pass through it and has length greater than $2$. William Cook's Lean 4 formalization in the Plectis repository (2026-09-14, revised 2026-09-22) treats the single member $s=10^{-6}$: the theorem erdos1041_counterexample bounds the total variation of any parametrized path joining two roots, and erdos1041_counterexample_hausdorff proves the stronger statement that every connected subset of the strict lemniscate containing two distinct roots has one-dimensional Hausdorff measure greater than $2$, which is the form of length the formal-conjectures statement uses; Cook reports that erdos1041_counterexample in the Assembly file compiles using only propext, Classical.choice and Quot.sound, and that most of the Lean was written by AI tools under Cook's direction. The formal-conjectures catalog marked the problem solved with answer false on 2026-09-23 and links the Hausdorff-length file as the formal proof, crediting the counterexample to ani.

Depends on. No page of this wiki.

Standing. Claimed. The user morluto wrote on 2026-09-09 that an independent check found a valid disproof, and Cook wrote on 2026-09-14 that every identity in the write-up is exact, adding two cautions: the $O(s^2)$ term has a coefficient near $2\times10^4$, so the picture only appears for $s$ below about $2\times10^{-5}$, and part (ii) of the write-up's component lemma fails as printed for $z^2$, so the formalization replaces it with explicit barrier curves in $\{\lvert f\rvert\ge1\}$ and the intermediate value theorem, while one inequality needs an added root hypothesis. Cook states that nobody independent has reviewed the formalization. No proof claim was registered on the site's proof-claims tab, the site labels the problem FALSIFIABLE (page last edited 06 December 2025), the community database records the problem falsifiable (status dated 2025-09-15, as of 2026-10-06), there is no refereed or arXiv version, and the corpus has built, replayed or audited nothing, so the formalized evidence kind is not listed. The two general proofs claimed earlier on the thread, ani 2026 and kasko37 2026, were rejected before this counterexample; the positive results for degrees at most four on [[problems/polynomials/E1041/claims/2026_09_18_borisov|Borisov 2026]] and [[problems/polynomials/E1041/claims/2026_06_23_pendyala|Pendyala 2026]] are consistent with it.