Erdős Problem 1120: Shortest path in polynomial sublevel sets

### What is the conjecture

Let $f \in \mathbb{C}[z]$ be a monic polynomial of degree $n$ with all roots satisfying $|z| \leq 1$. Define the sublevel set $E = \{z \in \mathbb{C} : |f(z)| \leq 1\}$. The question asks: What is the shortest length of a path in $E$ connecting the origin $z = 0$ to the unit circle $|z| = 1$?

The problem concerns the geometry of sublevel sets of polynomials whose roots lie in the closed unit disk. A trivial lower bound on the path length is 1 (achieved when $f(z) = z^n$). Erdős conjectured that the worst-case path length presumably tends to infinity with $n$, but not too fast.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1120, https://en.wikipedia.org/wiki/Erdős–Ko–Rado_theorem

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Complex polynomials and their evaluation
- Sublevel sets and geometric measure theory on $\mathbb{C}$
- Path length (arc length) in metric spaces

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of "shortest path length" in a geometric region (requires path integral/arc length formalization)
- Theory of polynomial sublevel sets and their connectivity properties in Mathlib

Rating justification (1-2 sentences): The statement involves fundamental objects (polynomials, complex numbers, sublevel sets) that exist in Mathlib, but formalizing the path length optimization and the geometric properties of sublevel sets would require moderate infrastructure development connecting geometric measure theory with polynomial analysis.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-30
* ams-12

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)