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

No current result

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

FormalConjectures/ErdosProblems/16.lean

Formal Conjectures

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.

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

Formalization
Erdős AI contributions wiki · 25 Feb, 2026
Machine
Antigravity, Gemini 3.1 Pro
Open the source record