Erdős problem 851
Let . Is there some such that the density of integers of the form , where and has at most prime divisors, is at least ?
Sources
FormalConjectures/ErdosProblems/
851.lean
Retained formal statement
The set of integers of the form 2^k+p (where p is prime) has positive lower density.
Formalisation note: here we also allow p = 1 since this simplifies the code and is equivalent to the original statement.
0 < (Erdos851.TwoPowAddSet 1).lowerDensitySolvedStatement only, no proof