Skip to content

Erdős problem 160

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 statement1 of 4

Estimate h(n)h(n) by finding a better lower bound.

FormalConjectures/ErdosProblems/160.leanErdos160.erdos_160.better_lower5 linesExact file
have lower_bound := sorry;(lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧  ∀ c > 0,    ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) →      ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound
OpenStatement only, no proof