Erdős problem 1074
Similarly, if is the set of all primes such that there exists an with such that , then does exist?
Sources
FormalConjectures/ErdosProblems/
1074.lean
Retained formal statement
Erdős, Hardy, and Subbarao proved that is infinite.
Formal proof linked here provided by AlphaProof.
Erdos1074.EHSNumbers.Infinite