Infinitely many primes $p$ with top prime factor of $\prod_{0\le i\le k}(p^2+i)$ equal to $p$? (Erdős #383)

Let $P(N)$ denote the largest prime factor of $N$. Is it true that for every fixed integer $k\geq 0$ there are infinitely many primes $p$ such that $$P\!\left(\prod_{0\leq i\leq k}(p^2+i)\right) = p\,?$$ Equivalently: are there infinitely many primes $p$ for which each of $p^2+1, p^2+2, \ldots, p^2+k$ is $p$-smooth (has no prime factor exceeding $p$)? The term $i=0$ contributes $p^2$, whose largest prime factor is $p$, so the condition is exactly that the $k$ succeeding integers are all $p$-smooth.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean — a statement formalisation already exists — preferred, else a full written proof) that for every fixed $k\geq 0$ there are infinitely many primes $p$ with $P(\prod_{0\leq i\leq k}(p^2+i))=p$; or a disproof for some $k$. Because 'infinitely many' cannot be settled by finite computation alone, a purely numerical submission cannot FULLY RESOLVE. ADVANCES (each independently checkable): an unconditional proof of the statement for a specific value of $k$ (even $k=1$ would be a breakthrough), with complete proof; OR a proof conditional on a clearly stated hypothesis (a smooth-values or Elliott–Halberstam-type input), with the conditional proof; OR a large reproducible search over primes $p\leq N$ tabulating, for each fixed small $k$, all $p$ with $p^2+1,\ldots,p^2+k$ all $p$-smooth, reporting the counts against the $1-\log 2$ heuristic, with source code and factorisation certificates. Deliver the proof file, the conditional proof, or the search code plus the tabulated witnesses and counts.