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$ ?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/333.lean

Formal Conjectures

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.

Reported by these sources. Not reviewed here.

AI alongside literature
Erdős AI contributions wiki · 25 Dec, 2025
Machine
Claude Opus 4.5, GPT-5.2 Pro
Open the source record
construction
VibeMathed
Machine
Claude Opus 4.5, GPT-5.2 Pro
Reported outcome
resolved
Open the source record