Skip to content

Erdős problem 17

Start work

Erdős Problem 17. Are there infinitely many cluster primes?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

17.lean

Retained formal statement3 of 4

In 2003, Elsholtz [El03] refined the upper bound to πC(x)≪x exp⁡ ⁣(−c(log⁡log⁡x)2)\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr) for every real 0<c<1/80 < c < 1/8.

[El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.

FormalConjectures/ErdosProblems/17.leanErdos17.erdos_17.variants.upper_Elsholtz5 linesExact file
∃ C,  0 < C ∧    ∀ c ∈ Set.Ioo 0 (1 / 8),      Asymptotics.IsBigOWith C Filter.atTop (fun x => ↑(Erdos17.clusterPrimeCount x)) fun x =>        ↑x * Real.exp (-c * Real.log (Real.log ↑x) ^ 2)
SolvedStatement only, no proof