Erdős Problem 677

Reference: erdosproblems.com/677

theorem Erdos677.lcmInterval_eq_example1 : Finset.lcmInterval 4 3 = Finset.lcmInterval 13 2 ∧ Finset.lcmInterval 3 4 = Finset.lcmInterval 19 2

Erdős expected very few solutions for $M(n, k) = M(m, l)$, where $m \geq n + k$ and $l > 1$. The only solutions he knew were the following.

theorem Erdos677.erdos_677 (m n k : ℕ) : k > 0 → m ≥ n + k → Finset.lcmInterval m k ≠ Finset.lcmInterval n k

Denote by $M(n, k)$ the least common multiple of the finite set $\{n+1, \dotsc, n+k\}$. Is it true that for all $m \geq n + k$, we get $M(m, k) \neq M(n, k)$?