Erdős problem 1028
Let where ranges over all functions . Estimate .
Sources
FormalConjectures/ErdosProblems/
1028.lean
Retained formal statement
Erdős and Spencer [ErSp71] proved that .
(fun n => ↑n ^ (3 / 2)) =O[Filter.atTop] fun n => ↑(Erdos1028.H n)SolvedStatement only, no proof