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

Start work

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/160.lean

Formal Conjectures

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

1have lower_bound := sorry;2(lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧3  ∀ c > 0,4    ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) →5      ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

OpenStatement only, no proof

Continue

Start a contribution Browse the source files Open the collection entry