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