Number theory
Erdős 11
Is every odd the sum of a squarefree number and a power of 2?References
No one has attempted this yet.
Formal statement
Lean type
∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ lWhat you must prove
import FormalConjectures.ErdosProblems.«11»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos11.erdos_11" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/11.lean
- Source type SHA-256
- sha256:7e9596e7603a5b3f536d79ee62512def1ce39a45e429cb460712833ba19ea738
- Task id
- fc-379fc029-erdos11-erdos-11-2bde7d8572-formalized-v1
- Task commitment
- sha256:d244b8473db45b9a7ad20467a664517222b6e450479c5d4f574901e4020a2b5a
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.