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 two powers of 2?
∀ (n : ℕ), Odd n → 1 < n → ∃ k l m, Squarefree k ∧ n = k + 2 ^ l + 2 ^ mOpenStatement only, no proof