Dead end: U61 (restart)

Settle Lemma.erdos_11: prove it or disprove it Method: Prove Lemma.erdos_11 or its negation: ∀ᶠ n : ℕ in atTop, Odd n → ∃ k l : ℕ, Squarefree k ∧ n = k + 2 ^ l. Question from Erdős problem 11 (https://www.erdosproblems.com/11): Is every large odd integer $n$ the sum of a squarefree number and a power of 2? Formal statement: formal-conjectures FormalConjectures/ErdosProblems/11.lean. Start from proofs/Lemma.erdos_11.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the lab's maintainers will report it upstream; say so in your notes. If neither is in reach, prove a useful special case or lemma, post what blocks you to the chat, and submit the files you started from unchanged, with notes on what you tried and what blocked you: the notebook keeps them as a dead end so others don't repeat it. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U61 dead end for Lemma.erdos_11. The statement is ℕ-valued: Squarefree 0 is false and l=0 is allowed (2^0=1). Odd n with l≥1 gives an odd k, so I found no edge case and the statement is faithful to Erdős #11. A chat note from U57 reports no counterexample to the variants for n<3·10^6 (the literature verifies much further). A covering-system disproof is blocked because square moduli p^2 cover too little density. This is a genuinely open problem. I am submitting the starting files unchanged. Statement checked: faithful Blocked by: out-of-reach Would unblock it: A proof would need a new sieve result showing that n-2^l is squarefree for some l ≤ log2 n, for all large odd n; a disproof would need an explicit infinite family of odd n where every n-2^l is non-squarefree (covering-congruence style), and none is known.

{"proofs":{}}