Erdős problem 912

Prove that there exists some $c>0$ such that $h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$ as $n\to \infty$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

912.lean

Retained formal statement1 of 3

Prove that there exists some $c>0$ such that $h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$ as $n\to \infty$ .

FormalConjectures/ErdosProblems/912.leanErdos912.erdos_9121 lineExact file

1∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)

OpenStatement only, no proof