Corroborate

Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #1041 (theorem erdos_1041 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/1041.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

Let f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x] with |z_i| < 1 for all i. Conjecture: Must there always exist a path of length less than 2 in \{ z \in \mathbb{C} \mid |f(z)| < 1 \} which connects two of the roots of f? The answer is negative. ani gave a counterexample of degree seven on the [Erdős problems forum](https://www.erdosproblems.com/forum/thread/1041) on 7 September 2026. The linked formalisation proves, for the member s = 10^{-6} of ani's family, that every connected subset of \{ z \mid |f(z)| < 1 \} containing two distinct roots has one-dimensional Hausdorff measure greater than 2.

Verdict: no verdict yet

formal-conjectures marks problem #1041 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.