Erdős Problem 9

Reference: erdosproblems.com/9

def Erdos9.Erdos9A : Set ℕ

The set of odd numbers that cannot be expressed as a prime plus two powers of 2.

Equations

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

theorem Erdos9.erdos9A_contains_one : 1 ∈ Erdos9A

theorem Erdos9.erdos9A_contains_three : 3 ∈ Erdos9A

theorem Erdos9.erdos9A_not_contains_five : 5 ∉ Erdos9A

theorem Erdos9.erdos_9_infinite : Erdos9A.Infinite

The set is known to be infinite. In [Er77c] Erdős credits Schinzel with proving that there are infinitely many odd integers not of this form, but gives no reference.

[Er77c] Erdős, P., Problems and results on combinatorial number theory. III..

theorem Erdos9.erdos_9 : 0 < Erdos9A.upperDensity ↔ sorry

Is the upper density of the set of odd numbers that cannot be expressed as a prime plus two powers of 2 positive?