Erdős Problem 1041

lengthdef

The length of a subset $s$ of $\mathbb{C}$ is defined to be its 1-dimensional Hausdorff measure $\mathcal{H}^1(s)$ .

noncomputable def length (s : Set ℂ) : ℝ≥0∞ := μH[1] s

exists_connected_component_contains_two_rootstheorem

Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If $f$ is a monic degree $n$ polynomial with all roots in the unit disk, then some connected component of $\{z \mid |f(z)| < 1\}$ contains at least two roots with multiplicity. See p. 139, above Problem 5: [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148.

theorem exists_connected_component_contains_two_roots :
    ∃ C, C ⊆ {z | ‖f.eval z‖ < 1} ∧ IsConnected C ∧
      2 ≤ (f.roots.filter (· ∈ C)).card := by
  sorry

erdos_1041theorem

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$ ?

theorem erdos_1041 :
    ∃ (z₁ z₂ : ℂ) (h : ({z₁, z₂} : Multiset ℂ) ≤ f.roots) (γ : Path z₁ z₂),
      Set.range γ ⊆ { z : ℂ | ‖f.eval z‖ < 1 } ∧ length (Set.range γ) < 2 := by
  sorry

goaldef

def goal : Prop :=
  ∃ C, C ⊆ {z | ‖f.eval z‖ < 1} ∧ IsConnected C ∧
      2 ≤ (f.roots.filter (· ∈ C)).card

import Conjectura.Problems.EP0003.Statement · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `ErdosProblems/1041.lean`. The problem is catalogued at https://www.erdosproblems.com/1041. LOCKED: solvers cannot modify this file.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits