Erdős problem 17 · problems.science

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

Sources

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

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

17.lean

Retained formal statement3 of 4

In 2003, Elsholtz [El03] refined the upper bound to $\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)$ for every real $0 < 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

1∃ C,2  0 < C ∧3    ∀ c ∈ Set.Ioo 0 (1 / 8),4      Asymptotics.IsBigOWith C Filter.atTop (fun x => ↑(Erdos17.clusterPrimeCount x)) fun x =>5        ↑x * Real.exp (-c * Real.log (Real.log ↑x) ^ 2)

SolvedStatement only, no proof

Sources

Search problems.science