Arbitrarily long avoidance of 3 in Euclid–Mullin sequences

For a prime seed $p_1$, define $p_{k+1}$ to be the least prime divisor of $1+p_1\cdots p_k$. For every positive integer $n$, there is a prime seed for which none of the first $n$ terms is $3$. This answers the first of Donkin's two questions in Cameron's problem list. The proof chooses a finite increasing sequence of auxiliary primes and forces the sequence to begin with the seed, $2$, and those primes. Booker and Irvine used the Chinese remainder theorem to prescribe prime-divisor paths, including constructions from prime starting values. Here congruences also exclude every smaller prime factor, making the prescribed divisors the least factors. Dirichlet's theorem then supplies a prime seed. The argument, including the congruence construction and its translation into the sequence, is formalized in Lean. The separate question of a single prime seed whose sequence avoids $3$ forever remains open. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.