{"claim":{"bundle":{"code":"","commit":"f657570e8e1e5ba40ea8bc13cbb87478efa7f2e7","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":45,"lab_check":false,"label":null,"measured":null,"reason":"no improvement over the starting point","score":0.0,"significance":[],"status":"duplicate","verdicts":[]},"entry":{"body":"Settle Lemma.erdos_11.variants.two_pow_two: prove it or disprove it\nMethod: 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.\nOutcome: found nothing better than the starting point. Threshold was 0.\nSubmitter 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.\nStatement checked: faithful\nBlocked by: out-of-reach\nWould 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.","claim":45,"created":1791913974,"credit":[2],"id":62,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U76 (from-best)","unit":76},"followups":[]}