Erdős Problem 16

References:

• erdosproblems.com/16
• [Ch23] Chen, Yong-Gao, A conjecture of Erdős on $p+2^k$. arXiv:2312.04120 (2023).
• [Er50] Erdős, P., On integers of the form $2^k+p$ and some related problems. Summa Brasil. Math. (1950), 113-123.
• [Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. (1934), 668-678.

def Erdos16.Erdos16Set : Set ℕ

The set of odd integers not of the form $2^k+p$.

Equations

• Erdos16.Erdos16Set = {n : ℕ | Odd n ∧ ¬∃ (k : ℕ) (p : ℕ), Nat.Prime p ∧ n = 2 ^ k + p}

def Erdos16.density_zero (S : Set ℕ) : Prop

A set of natural numbers has density 0.

Equations

• Erdos16.density_zero S = Filter.Tendsto (fun (x : ℕ) => ↑(Nat.count S x) / ↑x) Filter.atTop (nhds 0)

theorem Erdos16.erdos_16 : False ↔ ∃ (A : Set ℕ) (B : Set ℕ), Erdos16Set = A ∪ B ∧ (∃ (a : ℕ), ∃ d > 0, A = {x : ℕ | ∃ (m : ℕ), x = a + m * d}) ∧ density_zero B

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.

def Erdos16.positive_lower_density (S : Set ℕ) : Prop

A set of natural numbers has positive lower density.

Equations

• Erdos16.positive_lower_density S = (0 < Filter.liminf (fun (n : ℕ) => ↑↑(Nat.count S n) / ↑↑n) Filter.atTop)

theorem Erdos16.erdos_16.variant.romanoff : have S := {n : ℕ | Odd n ∧ ∃ (k : ℕ) (p : ℕ), Nat.Prime p ∧ n = 2 ^ k + p}; positive_lower_density S

Romanoff [Ro34] showed that the set of odd integers of this form has positive density.

theorem Erdos16.erdos_16.variant.erdos : ∃ (a : ℕ), ∃ d > 0, {x : ℕ | ∃ (m : ℕ), x = a + m * d} ⊆ Erdos16Set

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