Erdős problem 221
Is there a set such that, for all large , and such that every large integer can be written as for some and ?
Sources
FormalConjectures/ErdosProblems/
221.lean
Retained formal statement
Is there a set such that, for all large , and such that every large integer can be written as for some and ?
Lorentz [Lo54] proved there is such a set with, for all large , The answer is yes, proved by Ruzsa [Ru72].
True ↔ ∃ A, ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a