Erdős problem 160
On [Mathoverflow](https://mathoverflow.net/a/410815) user [leechlattice](https://mathoverflow.net/users/125498/leechlattice) shows that .
Sources
FormalConjectures/ErdosProblems/
160.lean
Retained formal statement
On [Mathoverflow](https://mathoverflow.net/a/410815) user [leechlattice](https://mathoverflow.net/users/125498/leechlattice) shows that .
(fun n => ↑(Erdos160.erdos_160.h n)) =O[Filter.atTop] fun n => ↑n ^ (2 / 3)SolvedStatement only, no proof