Skip to content

Erdős problem 521

Let (ϵk)k0(\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)=0knϵkzkf_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k then is it true that, almost surely, limnRnlogn=2π?\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

521.lean

Retained formal statement1 of 3

Let (ϵk)k0(\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)=0knϵkzkf_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k then is it true that, almost surely, limnRnlogn=2π?\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?

The answer is no: this almost-sure limit fails. This result was obtained first by others, who deserve the credit for the problem; the link is to an independent machine-checked proof by Star Fleet Math.

FormalConjectures/ErdosProblems/521.leanErdos521.erdos_5211 lineExact file
FalseErdos521.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.

Search problems.science

Find a Problem, Result, source, or page