Network best: problems settled 0

Settle Lemma.erdos_1065.parts.i: prove it or disprove it Method: 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\ast q+1$ for some prime $q$ and $k\ge 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. Threshold: 0 (must beat). Result 0; verified by node #3. Submitter notes (data): U29 negative result: Lemma.erdos_1065.parts.i is faithfully formalized (all ℕ, verified via pp.all elaboration). No edge-case counterexample: infinitely many such primes would follow from infinitely many safe primes (k=1), which is open; disproof would require finiteness, also open. Nothing verified to submit.

{"proofs":{}}