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

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

FormalConjectures/ErdosProblems/912.leanErdos912.erdos_912.variants.tao1 lineExact file
Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => √(2 * Real.pi) * (↑n / Real.log ↑n) ^ (1 / 2)
OpenStatement only, no proof