Skip to content

Erdős problem 521

Let (ϵk)k≥0(\epsilon_k)_{k\geq 0} be independently uniformly chosen at random from {−1,1}\{-1,1\}. If RnR_n counts the number of real roots of fn(z)=∑0≤k≤nϵkzkf_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k then is it true that, almost surely, lim⁡n→∞Rnlog⁡n=2π?\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/521.lean

Formal Conjectures

FormalConjectures/ErdosProblems/521.leanErdos521.erdos_5211 lineExact file
False ↔ Erdos521.Claim
SolvedProof has a holelean4formal statement referenceexternal 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

  • William Blair Lean proofswilliamjblair:Erdos521.erdos_521_negative

Reported activity

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

  • AI collaborating with humans

    Erdős AI contributions wiki · 30 Apr, 2026

    Machine
    GPT-5.5 Pro
    People
    Vjekoslav Kovač
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 25 Apr, 2026

    Machine
    GPT-5.5 Pro
    People
    Vjekoslav Kovač
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page