Erdős problem 31 · problems.science

Given any infinite set $A\subset \mathbb{N}$ there is a set $B$ of density $0$ such that $A+B$ contains all except finitely many integers.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

31.lean

Retained formal statement1 of 1

Given any infinite set $A\subset \mathbb{N}$ there is a set $B$ of density $0$ such that $A+B$ contains all except finitely many integers.

Conjectured by Erdős and Straus. Proved by Lorentz [Lo54].

FormalConjectures/ErdosProblems/31.leanErdos31.erdos_311 lineExact file

1∀ (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.