Does there exist a constant $c > 0$ such that, for all large $n$ and all polynomials $P$ of degree $n$ with coefficients $\pm 1$ , $∣ z ∣ = 1 max ∣ P (z)∣ > (1 + c) n ?$

Open — best to date is a honest null, not yet sealed.

analysis · open · formalized (Lean) · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

honest null

needs verification

attempted via frontier '?' (transfer_strength=n/a) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'n/a'. Do not re-attack cold; needs a new idea or richer accumulated context.

formal

AMS 12 30 · open (literature)

theorem erdos_1150 :
    answer(sorry) ↔ ∃ c > 0, ∀ᶠ n in Filter.atTop,
      ∀ P : ℂ[X],  (∀ i ≤ P.natDegree, P.coeff i = - 1 ∨ P.coeff i = 1) → P.natDegree = n →
        ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ > (1 + c) * Real.sqrt n

formal-conjectures/1150.lean ↗

status

open

evidence

formal

status

Search Vela