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
Is every odd the sum of a squarefree number and a power of 2?
∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ lOpenStatement only, no proof