Dead end: U41 (vary)

Settle Lemma.erdos_1065.parts.ii: prove it or disprove it Method: 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\ge 0$, $l\ge 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. Outcome: found nothing better than the starting point. Threshold was 0. Submitter 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.

{"proofs":{}}