Erdős problem 16

Is the set of odd integers not of the form $2^k+p$ the union of an infinite arithmetic progression and a set of density $0$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

16.lean

Retained formal statement2 of 3

Using covering congruences Erdős [Er50] proved that the set of odd integers which are not of this form contains an infinite arithmetic progression.

FormalConjectures/ErdosProblems/16.leanErdos16.erdos_16.variant.erdos1 lineExact file

1∃ a, ∃ d > 0, {x | ∃ m, x = a + m * d} ⊆ Erdos16.Erdos16Set

SolvedStatement only, no proof