Can the product of a coprime arithmetic progression of length at least 4 be a perfect power? (Erdős #672)

Let $k\geq 4$ and let $n,n+d,\ldots,n+(k-1)d$ be an arithmetic progression of positive integers with $\gcd(n,d)=1$. Can the product $n(n+d)\cdots(n+(k-1)d)$ be a perfect power $m^{\ell}$ (integers $m,\ell\geq 2$)? Both restrictions are essential: Pell equations give infinitely many coprime pairs $n,d$ with $n(n+d)(n+2d)$ a perfect square, and over the integers in general there are examples such as $(-6)\cdot(-1)\cdot 4\cdot 9=6^3$ (observed by Führer).

Acceptance. FULLY RESOLVES (yes direction): explicit positive integers $n,d,k,m,\ell$ with $k\geq 4$ (necessarily $k\geq 35$ given the background), $\gcd(n,d)=1$, $m,\ell\geq 2$, together with a machine-verifiable check of the identity $n(n+d)\cdots(n+(k-1)d)=m^{\ell}$. FULLY RESOLVES (no direction): a proof that no such perfect-power product exists for any $k\geq 4$ — machine-checkable (Lean/Coq; the statement is formalized in the DeepMind formal-conjectures repository) preferred, else a complete written proof with all steps. ADVANCES: a proof extending the excluded range strictly beyond the $4\leq k\leq 34$ record stated in the background (e.g. settling $k=35$, or all $k\leq K$ for a new explicit $K$), with any computer-assisted steps fully reproducible; or weakening the largeness/primality conditions in the Bennett–Siksek regime with proof; or a reproducible certified search establishing there is no solution with all terms below an explicit bound. Deliver the witness tuple plus verification script, or the proof file, or the computation code plus certificates and a precise statement of the range settled.