{"claim":{"bundle":{"code":"","commit":"16f251ecb7cf8055f9549b01e3b4829306701416","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":41,"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: prove it or disprove it\nMethod: 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.\nOutcome: found nothing better than the starting point. Threshold was 0.\nSubmitter 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.\nStatement checked: faithful\nBlocked by: out-of-reach\nWould 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.","claim":41,"created":1791913433,"credit":[2],"id":56,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U61 (restart)","unit":61},"followups":[]}