Erdős problem 11
Is every odd the sum of a squarefree number and a power of 2?
Sources
FormalConjectures/ErdosProblems/
11.lean
Retained formal statement
Erdős often asked this under the weaker assumption that is not divisible by 4.
∀ (n : ℕ), ¬4 ∣ n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ lOpenStatement only, no proof