Grimm's conjecture: distinct prime divisors for the consecutive composites $n+1,\ldots,n+k$ (Erdős #375)

Is it true that for any $n,k\geq 1$, if $n+1,\ldots,n+k$ are all composite then there are distinct primes $p_1,\ldots,p_k$ such that $p_i\mid n+i$ for $1\leq i\leq k$? Equivalently: the family of sets $S_i=\{p \text{ prime}: p\mid n+i\}$ for a run of consecutive composites always admits a system of distinct representatives (in Hall's-theorem language, no subfamily of $j$ of the $S_i$ has union smaller than $j$). It suffices to check maximal runs, i.e. the composites strictly between consecutive primes. A single run of consecutive composites admitting no such choice of distinct primes would disprove the conjecture.

Acceptance. FULLY RESOLVES (disproof): an explicit $n$ and $k$ with $n+1,\ldots,n+k$ all composite, together with a machine-checkable Hall-violation certificate: a subset $J\subseteq\{1,\ldots,k\}$ such that the union of the prime-divisor sets $\{p: p\mid n+i\}$, $i\in J$, has fewer than $|J|$ elements, plus the factorizations of the $n+i$ and code that verifies compositeness and the violation. FULLY RESOLVES (proof): a complete proof of the conjecture for all $n,k$; machine-checkable (Lean, against the existing formal-conjectures statement) preferred, else a full written proof (note it must inherently prove strong prime-gap bounds — a computation alone cannot close it). ADVANCES: (a) extend the exhaustive verification strictly beyond the best bound stated in the background, with the sieve + matching code, the attained bound, and a reproducible exhaustiveness recipe; (b) verify the conjecture for all record prime gaps in a stated large range (gap lists are public), with factorizations and matchings archived; or (c) an asymptotic improvement of the $k\ll(\log n/\log\log n)^3$ range from the background, with proof. Deliver the counterexample certificate, or the verification code + attained bound + certificates, or the proof file.