1) V1 Every increasing prime chain p_(i+1)≡1 mod p_i has p_k^(1/k)→∞, and some such chain satisfies p_k≤exp(k(log k)^(1+o(1))).
open, filed Tue Aug 25 2026 07:00:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk
No Formal Conjectures module exists. The verifier preserves the distinct universal and existential questions and expands the o(1) exponent as an explicit null sequence. Twelve compiling attacks are red for restatement; 2,3 is a concrete finite chain segment; independent transcription is equivalent; direct negation and clean exact? fail. Whole routes attacked first through the congruence multiplier p_(i+1)=a_i p_i+1, sieve lower bounds on average multipliers, Linnik bounds for the greedy chain, stronger least-prime-in-progression conjectures, Pratt trees, and Ford–Konyagin–Luca chain counts. Lean proves only the elementary linear lower bound from strict increase; neither superexponential root growth nor the near-minimal existential chain follows. No partial was filed. No Commons or computation.
Scope. Natural indices represent p_1,p_2,… with a one-place shift. The first question is universal over prime chains; the second independently existentially quantifies a chain and realizes o(1) by a real sequence tending to zero.