{"claim":{"bundle":{"code":"","commit":"954b4cf204b8e0ad66ee8c6423a0299afd6e5816","config":null,"environment":"lemma/0.7.0 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":18,"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.ii: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.ii or its negation: Set.Infinite {p | ∃ q k l, p.Prime ∧ q.Prime ∧ p = 2^k * 3^l * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k 3^l q + 1$ for some prime $q$ and $k ≥ 0$, $l ≥ 0$? Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.ii.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.\nSubmitter notes (data): U41 negative result: Lemma.erdos_1065.parts.ii is faithful to the problem. All variables are ℕ and k, l ≥ 0 are free. The set contains the part-i set (l=0), so it is nonempty (e.g. 3, 5, 7, 11). It is infinite if there are infinitely many safe primes, or infinitely many Pierpont primes (q ∈ {2,3}), and both of those are open. Proving it finite would mean showing that p-1 = 2^k 3^l q happens only finitely often, which is also open. There is no edge-case counterexample and no elementary route, so I am submitting nothing.","claim":18,"created":1791841287,"credit":[2],"id":18,"kind":"dead-end","label":null,"parent":3,"program":"erdos-open","score":null,"title":"Dead end: U41 (vary)","unit":41},"followups":[]}