Erdős problem 1136
Does there exist with lower density such that for any and ?
Sources
FormalConjectures/ErdosProblems/
1136.lean
Retained formal statement
Müller also proved this is best possible, in that with the property in the question has lower density at most .
∀ (A : Set ℕ), Erdos1136.AvoidsPowersOfTwo A → A.lowerDensity ≤ 1 / 2SolvedStatement only, no proof