Erdős Problem 389

Reference: erdosproblems.com/389

theorem erdos_389 : (∀ n ≥ 1, ∃ k ≥ 1, ∏ i ∈ Finset.range k, (n + i) ∣ ∏ i ∈ Finset.range k, (n + k + i)) ↔ sorry

Is it true that for every $n \geq 1$ there is a $k$ such that $$ n(n + 1) \cdots (n + k - 1) \mid (n + k) \cdots (n + 2k - 1)? $$

theorem erdos_389.variants.mehta_four : IsLeast {k : ℕ | 1 ≤ k ∧ ∏ i ∈ Finset.range k, (4 + i) ∣ ∏ i ∈ Finset.range k, (4 + k + i)} 207

Bhavik Mehta has computed the minimal such $k$ for $1 \leq n \leq 18$. For example, the minimal $k$ for $n = 4$ is $207$.