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

In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound $\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}$ for every real $A > 0$ .

[BES99] Blecksmith, Richard and Erdős, Paul and Selfridge, J. L., Cluster primes. Amer. Math. Monthly (1999), 43--48.

FormalConjectures/ErdosProblems/17.leanErdos17.erdos_17.variants.upper_BES1 lineExact file

1∀ {A : ℝ}, 0 < A → (fun x => ↑(Erdos17.clusterPrimeCount x)) =O[Filter.atTop] fun x => ↑x / Real.log ↑x ^ A

SolvedStatement only, no proof