{"claim":{"bundle":{"code":"","commit":"5222a1f0d224c65a323a055499967cd2ea3c0d34","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":42,"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.all_odd: prove it or disprove it\nMethod: Prove Lemma.erdos_11.variants.all_odd or its negation: ∀ (n : ℕ) (hn : Odd n) (hn' : 1 < n), ∃ k l : ℕ, Squarefree k ∧ n = k + 2 ^ l. Conjecture from Erdős problem 11 (https://www.erdosproblems.com/11): Every odd $n > 1$ is the sum of a squarefree number and a power of 2. This is the form in earlier versions of erdosproblems.com/11 and the hypothesis of [GrSo98]. It is stronger than `erdos_11`, which asks only about large $n$: a single exception would refute it. Formal statement: formal-conjectures FormalConjectures/ErdosProblems/11.lean. Start from proofs/Lemma.erdos_11.variants.all_odd.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): U74 dead end for Lemma.erdos_11.variants.all_odd. The statement is ℕ-valued. Squarefree 0 is false and l=0 is allowed, so there is no edge case: n=3 works as 1+2. The formalization is faithful to the GrSo98 hypothesis. U57 found no counterexample for n<3·10^6 (chat), and the literature verifies much further. A disproof would need a finite counterexample beyond the verified range, which is not computationally reachable here. Submitting the starting files unchanged.\nStatement checked: faithful\nBlocked by: out-of-reach\nWould unblock it: A proof needs a sieve result that n-2^l is squarefree for some l for every odd n>1, which nobody has. A disproof needs an explicit counterexample, and a covering-style family is impossible because the p^2 moduli cover too little density.","claim":42,"created":1791913455,"credit":[2],"id":57,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U74 (restart)","unit":74},"followups":[]}