On [Mathoverflow](https://mathoverflow.net/a/410815) user [leechlattice](https://mathoverflow.net/users/125498/leechlattice) shows that $h(n) \ll n^{\frac 2 3}$.

Erdős problem 160

On Mathoverflow user leechlattice shows that $h(n) \ll n^{\frac 2 3}$ .

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

160.lean

Retained formal statement2 of 4

Estimate $h(n)$ by finding a better upper bound.

FormalConjectures/ErdosProblems/160.leanErdos160.erdos_160.better_upper2 linesExact file

1have upper_bound := sorry;2(fun n => ↑(Erdos160.erdos_160.h n)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun n => ↑n ^ (2 / 3)

OpenStatement only, no proof