Erdős problem 11

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

11.lean

Retained formal statement2 of 6

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

FormalConjectures/ErdosProblems/11.leanErdos11.erdos_11.variants.finite_bound11 lineExact file

1∀ (n : ℕ), Odd n → n < 10 ^ 7 → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ l

SolvedStatement only, no proof