Erdős problem 16 · problems.science

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

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

16.lean

Retained formal statement1 of 3

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

Erdős called this conjecture "rather silly".

Chen [Ch23] has proved the answer is no.

This was formalized in Lean by Chin using Aristotle.

FormalConjectures/ErdosProblems/16.leanErdos16.erdos_161 lineExact file

1False ↔ ∃ A B, Erdos16.Erdos16Set = A ∪ B ∧ (∃ a, ∃ d > 0, A = {x | ∃ m, x = a + m * d}) ∧ Erdos16.density_zero 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.