Skip to content

Erdős problem 115

If p(z)p(z) is a polynomial of degree nn such that {z:∣p(z)∣≤1}\{z : \lvert p(z)\rvert\leq 1\} is connected then is it true that max⁡z∈C∣p(z)∣≤1∣p′(z)∣≤(12+o(1))n2?\max_{\substack{z\in\mathbb{C}\\ \lvert p(z)\rvert\leq 1}} \lvert p'(z)\rvert \leq (\tfrac{1}{2}+o(1))n^2?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/115.lean

Formal Conjectures

FormalConjectures/ErdosProblems/115.leanErdos115.erdos_1159 linesExact file
True ↔  ∀ ε > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (p : Polynomial ℂ),        p.Monic →          p.natDegree = n →            IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} →              ∀ (z : ℂ),                ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:115
  • PLBY Lean proofsErdosProblems.Erdos115

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • Formalization

    Erdős AI contributions wiki · 3 Mar, 2026

    Machine
    Aristotle, Claude Opus 4.6, Claude Sonnet 4.6, Gemini 3 Flash, Gemini 3.1 Pro, ulam.ai scaffold with Gemini 3 Flash and Gemini 3.1 Pro
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page