Erdős problem 333

Let $A\subseteq \mathbb{N}$ be a set of density zero. Does there exist a $B$ such that $A\subseteq B+B$ and $\lvert B\cap \{1,\ldots,N\}\rvert =o(N^{1/2})$ for all large $N$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

333.lean

Retained formal statement1 of 1

Let $A\subseteq \mathbb{N}$ be a set of density zero. Does there exist a $B$ such that $A\subseteq B+B$ and $\lvert B\cap \{1,\ldots,N\}\rvert =o(N^{1/2})$ for all large $N$ ?

The answer is no. Erdős and Newman [ErNe77] have proved this is true when $A$ is the set of squares. In fact, Theorem 2 of [ErNe77] already implies a negative answer to this problem, but this seems to have been overlooked by Erdős and Graham.

See also [806].

FormalConjectures/ErdosProblems/333.leanErdos333.erdos_3332 linesExact file

1False ↔2  ∀ (A : Set ℕ), A.HasDensity 0 → ∃ B, A ⊆ B + B ∧ (fun N => ↑(B ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => √↑N

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.