Erdős problem 522 · problems.science

For $P_n(z) = \sum_{k=0}^n \varepsilon_k z^k$ with independent uniform signs, does the number $R_n$ of roots in $|z| \le 1$ satisfy $R_n/(n/2) \to 1$ almost surely? The manuscript proves the strong law with $R_n = n/2 + O_\omega(n^{149/150})$ .

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/522.lean

Formal Conjectures

FormalConjectures/ErdosProblems/522.leanErdos522.erdos_5224 linesExact file

1True ↔2  ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]3    (c : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),4    MeasureTheory.volume {ω | Filter.Tendsto (fun n => 2 * ↑(c.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} = 1

OpenStatement only, no proof

Proof manifests naming this Problem

William Blair Lean proofswilliamjblair:Erdos522.erdos_522

Reported activity

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

argument
VibeMathed
Machine
GPT-5.5 Pro
Reported outcome
candidate
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science