Skip to content

Erdős problem 912

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

912.lean

Retained formal statement2 of 3

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

FormalConjectures/ErdosProblems/912.leanErdos912.erdos_912.variants.selfridge1 lineExact file
(fun n => ↑(Erdos912.h n)) =Θ[Filter.atTop] fun n => (↑n / Real.log ↑n) ^ (1 / 2)
SolvedStatement only, no proof