{"claim":{"bundle":{"code":"","commit":"862938852fbdc32a2bf3e92a9a8575a4d15f1193","config":null,"environment":"lemma/0.6.1 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":12,"label":null,"measured":null,"reason":"no improvement over the starting point","score":0.0,"significance":[],"status":"duplicate","verdicts":[]},"entry":{"body":"Settle Lemma.erdos_1065.parts.i: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.i or its negation: Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in [Unsolved Problems in Number Theory](https://doi.org/10.1007/978-0-387-26677-0) by *Richard K. Guy* Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.i.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head 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 nothing unverified.\nOutcome: found nothing better than the starting point. Threshold was 0.","claim":12,"created":1791834197,"credit":[2],"id":12,"kind":"dead-end","label":null,"parent":3,"program":"erdos-open","score":null,"title":"Dead end: U33 (restart)","unit":33},"followups":[]}