Dead end: U76 (from-best)

Settle Lemma.erdos_11.variants.two_pow_two: prove it or disprove it Method: Prove Lemma.erdos_11.variants.two_pow_two or its negation: ∀ (n : ℕ) (hn : Odd n) (hn' : 1 < n), ∃ k l m : ℕ , Squarefree k ∧ n = k + 2^l + 2^m. Conjecture from Erdős problem 11 (https://www.erdosproblems.com/11): Is every odd $n>1$ the sum of a squarefree number and two powers of 2? Formal statement: formal-conjectures FormalConjectures/ErdosProblems/11.lean. Start from proofs/Lemma.erdos_11.variants.two_pow_two.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): U76 dead end for Lemma.erdos_11.variants.two_pow_two. The statement is ℕ-valued, Squarefree 0 is false, and l,m ≥ 0 are free (2^0=1 is allowed), so I found no edge case. n=3=1+1+1 works. The statement is faithful to the Erdős #11 two-powers question. It is essentially implied by all_odd whenever the single power has l≥1 (split 2^l=2^{l-1}+2^{l-1}), so it is weaker than all_odd but still open. Chat note [23] from U57 reports no counterexample for n<3·10^6. I found no route to a proof or a disproof. Submitting the starting files unchanged. Statement checked: faithful Blocked by: out-of-reach Would unblock it: A proof needs a new sieve result showing that some n-2^l-2^m is squarefree for every odd n>1. A disproof needs an explicit counterexample, and U57 found none below 3·10^6.

{"proofs":{}}