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

9797 is the smallest prime that is not a cluster prime.

FormalConjectures/ErdosProblems/17.leanErdos17.isClusterPrime_97_isLeast_non_cluster1 lineExact file
IsLeast {p | Nat.Prime p ∧ ¬Erdos17.IsClusterPrime p} 97
TestStatement only, no proof