Erdős Problem 11

Reference: erdosproblems.com/11

theorem Erdos11.erdos_11 (n : ℕ) (hn : Odd n) (hn' : 1 < n) : ∃ (k : ℕ) (l : ℕ), Squarefree k ∧ n = k + 2 ^ l

Is every odd $n > 1$ the sum of a squarefree number and a power of 2?

theorem Erdos11.erdos_11.variants.not_four_dvd (n : ℕ) (hn : ¬4 ∣ n) (hn' : 1 < n) : ∃ (k : ℕ) (l : ℕ), Squarefree k ∧ n = k + 2 ^ l

Erdős often asked this under the weaker assumption that $n > 1$ is not divisible by 4.

theorem Erdos11.erdos_11.variants.two_pow_two (n : ℕ) (hn : Odd n) (hn' : 1 < n) : ∃ (k : ℕ) (l : ℕ) (m : ℕ), Squarefree k ∧ n = k + 2 ^ l + 2 ^ m

Is every odd $n > 1$ the sum of a squarefree number and two powers of 2?

theorem Erdos11.erdos_11.variants.finite_bound1 (n : ℕ) (hn : Odd n) (h : n < 10 ^ 7) (hn' : 1 < n) : ∃ (k : ℕ) (l : ℕ), Squarefree k ∧ n = k + 2 ^ l

Every odd $1 < n < 10^7$ is the sum of a squarefree number and a power of 2.

theorem Erdos11.erdos_11.variants.finite_bound2 (n : ℕ) (hn : Odd n) (h : n < 2 ^ 50) (hn' : 1 < n) : ∃ (k : ℕ) (l : ℕ), Squarefree k ∧ n = k + 2 ^ l

Every odd $1 < n < 2^50$ is the sum of a squarefree number and a power of 2.

theorem Erdos11.erdos_11.variants.granville_soundararajan (H : ∀ (n : ℕ), Odd n → 1 < n → ∃ (k : ℕ) (l : ℕ), Squarefree k ∧ n = k + 2 ^ l) : {p : ℕ | Nat.Prime p ∧ 2 ^ p ≡ 2 [MOD p ^ 2]}.Infinite

Suppose that every odd $n$ is the sum of a squarefree number and a power of 2. Then the set of primes $p$ such that $2 ^ p ≡ 2 \mod p ^ 2$ is infinite. This is Theorem 1 in [GrSo98]. [GrSo98] Granville, A. and Soundararajan, K., A Binary Additive Problem of Erdős and the Order of $2$ mod $p^2$. The Ramanujan Journal (1998), 283-298.