Erdős problem 912 · problems.science

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$ .

No current result

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

FormalConjectures/ErdosProblems/912.lean

Formal Conjectures

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