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
Let . Is there some such that the density of integers of the form , where and has at most prime divisors, is at least ?
This was proved affirmatively by Price and GPT-5.2 Pro [Pr26].
∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ dSolvedStatement only, no proof