Skip to content

Erdős problem 160

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

160.lean

Retained formal statement4 of 4

The observation of Zachary Hunter in that question coupled with the bounds of Kelley-Meka KeMe23 imply that h(N)≫exp⁡(c(log⁡N)112)h(N) \gg \exp(c(\log N)^{\frac 1 {12}}) for some c>0c > 0.

FormalConjectures/ErdosProblems/160.leanErdos160.erdos_160.variants.known_lower1 lineExact file
∃ 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