Skip to content

Erdős problem 333

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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/333.lean

Formal Conjectures

FormalConjectures/ErdosProblems/333.leanErdos333.erdos_3332 linesExact file
False ↔  ∀ (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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:333
  • PLBY Lean proofsErdosProblems.Erdos333

Reported activity

Work these sources record against this Problem. Source-reported attribution, 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

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page