Erdős Problem 727

Reference: erdosproblems.com/727

theorem erdos_727 : (∀ k ≥ 2, {n : ℕ | (n + k).factorial ^ 2 ∣ (2 * n).factorial}.Infinite) ↔ sorry

Let $k ≥ 2$. Does $((n+k)!)^2∣(2n)!$ hold for infinitely many $n$?

theorem erdos_727_variants.k_2 : {n : ℕ | (n + 2).factorial ^ 2 ∣ (2 * n).factorial}.Infinite ↔ sorry

It is open even for $k = 2$. Let $k = 2$. Does $((n+k)!)^2∣(2n)!$ hold for infinitely many n?

theorem erdos_727_variants.k_1 : {n : ℕ | (n + 1).factorial ^ 2 ∣ (2 * n).factorial}.Infinite ↔ True

Balakran proved this holds for $k = 1$.

Let $k = 1$. Does $((n+k)!)^2∣(2n)!$ for infinitely many $n$?

theorem erdos_727_variants.k_1_2 (k : ℕ) (hk : 2 ≤ k) : {n : ℕ | (n + k).factorial * (n + 1).factorial ∣ (2 * n).factorial}.Infinite

Erdős, Graham, Ruzsa, and Straus observe that the method of Balakran can be further used to prove that there are infinitely many $n$ such that $(n+k)!(n+1)!∣(2n)!$