Erdős problem 160 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

160.lean

Retained formal statement4 of 4

The observation of Zachary Hunter in [that question](https://mathoverflow.net/q/410808) coupled with the bounds of Kelley-Meka [KeMe23](https://arxiv.org/abs/2302.05537) imply that $h(N) \gg \exp(c(\log N)^{\frac 1 {12}})$ for some $c > 0$ .

FormalConjectures/ErdosProblems/160.leanErdos160.erdos_160.variants.known_lower1 lineExact file

1∃ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)

SolvedStatement only, no proof

Sources

Search problems.science