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
Regarding the first question, Hardy and Subbarao computed all EHS numbers up to , and write "...if this trend conditions we expect [the limit] to be around 0.5, if it exists."
Erdos1074.EHSNumbers.HasDensity (1 / 2)OpenStatement only, no proof