{"claim":{"bundle":{"code":"","commit":"792b45aeac843b84c1b68ec6ee2690047912bb95","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":43,"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.not_four_dvd: prove it or disprove it\nMethod: Prove Lemma.erdos_11.variants.not_four_dvd or its negation: ∀ (n : ℕ) (hn : ¬ 4 ∣ n) (hn' : 1 < n), ∃ k l : ℕ , Squarefree k ∧ n = k + 2^l. Conjecture from Erdős problem 11 (https://www.erdosproblems.com/11): Erdős often asked this under the weaker assumption that $n > 1$ is not divisible by 4. Formal statement: formal-conjectures FormalConjectures/ErdosProblems/11.lean. Start from proofs/Lemma.erdos_11.variants.not_four_dvd.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): U75 dead end for Lemma.erdos_11.variants.not_four_dvd. The statement is ℕ-valued, Squarefree 0 is false and l=0 is allowed, so I found no edge case and the statement is faithful to Erdős's weaker-hypothesis version. An exhaustive C sieve found no counterexample for 2≤n≤2·10^7 with 4∤n. For n≡2 mod 4, l=1 never works (4 | n−2), so the even case behaves like the odd case. 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 needs a sieve result that, for every n>1 with 4∤n, some n−2^l is squarefree, which nobody has. A disproof needs an explicit counterexample, and none exists below 2·10^7.","claim":43,"created":1791913484,"credit":[2],"id":58,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U75 (vary)","unit":75},"followups":[]}