Are there only finitely many equal products of two disjoint blocks of 4+ consecutive integers? (Erdős #388)

For positive integers $m_1,m_2,k_1,k_2$ consider when two products of consecutive integers coincide: $$\prod_{1\leq i\leq k_1}(m_1+i)=\prod_{1\leq j\leq k_2}(m_2+j),$$ i.e. $(m_1+1)(m_1+2)\cdots(m_1+k_1)=(m_2+1)(m_2+2)\cdots(m_2+k_2)$. Restrict to $k_1,k_2>3$ (each block has at least four terms) and $m_1+k_1\leq m_2$, so the two blocks of consecutive integers are disjoint, with the first lying entirely below the second. Can one classify all solutions, and in particular are there only finitely many? More generally, Erdős conjectured that for any fixed positive integers $a,b$ and any fixed $k_1>2$, the weighted equation $a\prod_{1\leq i\leq k_1}(m_1+i)=b\prod_{1\leq j\leq k_2}(m_2+j)$ has only finitely many solutions.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise a fully detailed written proof) that the equation with $k_1,k_2>3$ and $m_1+k_1\leq m_2$ has only finitely many solutions — ideally exhibiting the explicit finite list of all solutions together with a proof the list is complete — OR a proof that infinitely many solutions exist (e.g. an explicit infinite parametric family, verified). ADVANCES: (a) exhibit a previously-unrecorded solution, i.e. specific $(m_1,k_1,m_2,k_2)$ with both blocks of length $\geq 4$, disjoint, and equal product, delivering the prime factorizations of both products as a machine-checkable witness; (b) an exhaustive computer search certifying there is no solution with $m_2+k_2\leq N$ for a stated bound $N$, delivered with the search program and a reproducible exhaustiveness certificate; (c) a conditional finiteness proof under a clearly-flagged hypothesis (e.g. abc), or an unconditional finiteness proof for a restricted shape (fixed $k_1,k_2$). Deliver the witness with factorizations, the search code plus certified bound, or the proof file.