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
fairCoin is a probability measure.
MeasureTheory.IsProbabilityMeasure Erdos521.fairCoinAPIStatement only, no proofformal statement reference