Erdős problem 221

Is there a set $A\subset\mathbb{N}$ such that, for all large $N$ , $\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N$ and such that every large integer can be written as $2^k+a$ for some $k\geq 0$ and $a\in A$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

221.lean

Retained formal statement1 of 1

Is there a set $A\subset\mathbb{N}$ such that, for all large $N$ , $\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N$ and such that every large integer can be written as $2^k+a$ for some $k\geq 0$ and $a\in A$ ?

Lorentz [Lo54] proved there is such a set with, for all large $N$ , $\lvert A\cap\{1,\ldots,N\}\rvert \ll \frac{\log\log N}{\log N}N$ The answer is yes, proved by Ruzsa [Ru72].

FormalConjectures/ErdosProblems/221.leanErdos221.erdos_2214 linesExact file

1True ↔2  ∃ A,3    ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧4      ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.