Skip to content

Erdős problem 31

Given any infinite set A⊂NA\subset \mathbb{N} there is a set BB of density 00 such that A+BA+B contains all except finitely many integers.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/31.lean

Formal Conjectures

FormalConjectures/ErdosProblems/31.leanErdos31.erdos_311 lineExact file
∀ (A : Set ℕ), A.Infinite → ∃ B, B.HasDensity 0 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, n ∈ A + B
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:31
  • PLBY Lean proofsErdosProblems.Erdos31

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page