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 statement2 of 3

Erdős and Selfridge prove in [Er82c] that $h(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}$ .

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

1(fun n => ↑(Erdos912.h n)) =Θ[Filter.atTop] fun n => (↑n / Real.log ↑n) ^ (1 / 2)

SolvedStatement only, no proof