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

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

912.lean

Retained formal statement3 of 3

A heuristic of Tao using the Cramér model for the primes suggests this is true with $c=\sqrt{2\pi}$ .

FormalConjectures/ErdosProblems/912.leanErdos912.erdos_912.variants.tao1 lineExact file

1Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => √(2 * Real.pi) * (↑n / Real.log ↑n) ^ (1 / 2)

OpenStatement only, no proof