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

In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound πC(x)≪Ax(log⁡x)−A\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A} for every real A>0A > 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
∀ {A : ℝ}, 0 < A → (fun x => ↑(Erdos17.clusterPrimeCount x)) =O[Filter.atTop] fun x => ↑x / Real.log ↑x ^ A
SolvedStatement only, no proof