Erdős problem 521
Let be independently uniformly chosen at random from . If counts the number of real roots of then is it true that, almost surely,
Sources
FormalConjectures/ErdosProblems/
521.lean
Retained formal statement
Let be independently uniformly chosen at random from . If counts the number of real roots of then is it true that, almost surely,
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.
False ↔ Erdos521.Claim