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