Erdős Problem 10

Reference: erdosproblems.com/10

@[reducible, inline]

abbrev Erdos10.sumPrimeAndTwoPows (k : ℕ) : Set ℕ

The set of natural numbers that can be written as a sum of a prime and at most $k$ powers of $2$.

Equations

• Erdos10.sumPrimeAndTwoPows k = {x : ℕ | ∃ (p : ℕ) (pows : Multiset ℕ) (_ : Nat.Prime p) (_ : pows.card ≤ k), p + (Multiset.map (fun (x : ℕ) => 2 ^ x) pows).sum = x}

theorem Erdos10.erdos_10 : (∃ (k : ℕ), sumPrimeAndTwoPows k = Set.univ \ {0, 1}) ↔ sorry

Is there some $k$ such that every integer is the sum of a prime and at most $k$ powers of $2$?

theorem Erdos10.erdos_10.variants.gallagher (ε : ℝ) (hε : 0 < ε) : ∃ (k : ℕ), 1 - ε ≤ (sumPrimeAndTwoPows k).lowerDensity

Gallagher [Ga75] has shown that for any $ϵ > 0$ there exists $k(ϵ)$ such that the set of integers which are the sum of a prime and at most $k(ϵ)$ many powers of $2$ has lower density at least $1 - ϵ$.

Ref: Gallagher, P. X., Primes and powers of 2.

theorem Erdos10.erdos_10.variants.granville_soundararajan_odd : {n : ℕ | Odd n ∧ 1 < n} ⊆ sumPrimeAndTwoPows 3 ∧ {n : ℕ | Even n ∧ n ≠ 0} ⊆ sumPrimeAndTwoPows 4

Granville and Soundararajan [GrSo98] have conjectured that at most $3$ powers of $2$ suffice for all odd integers, and hence at most $4$ powers of $2$ suffice for all even integers.

Ref: Granville, A. and Soundararajan, K., A Binary Additive Problem of Erdős and the Order of $2$ mod $p^2$

theorem Erdos10.erdos_10.variants.grechuk_example : 1117175146 ∉ sumPrimeAndTwoPows 3

Bogdan Grechuk has observed that 1117175146 is not the sum of a prime and at most $3$ powers of $2$.

theorem Erdos10.erdos_10.variants.two_pows : ({n : ℕ | Even n} \ sumPrimeAndTwoPows 2).Infinite

There are infinitely many even integers not the sum of a prime and $2$ powers of $2$

theorem Erdos10.erdos_10.variants.gretchuk : ({n : ℕ | Even n} \ sumPrimeAndTwoPows 3).Infinite

Bogdan Grechuk has observed that $1117175146$ is not the sum of a prime and at most $3$ powers of $2$, and pointed out that parity considerations, coupled with the fact that there are many integers not the sum of a prime and $2$ powers of $2$ suggest that there exist infinitely many even integers which are not the sum of a prime and at most $3$ powers of $2$).