Erdős problem 389

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)?$

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

389.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/389.leanErdos389.erdos_389.variants.mehta_four1 lineExact file

1IsLeast {k | 1 ≤ k ∧ ∏ i ∈ Finset.range k, (4 + i) ∣ ∏ i ∈ Finset.range k, (4 + k + i)} 207

TextbookStatement only, no proof