Erdős Problem 376

Reference: erdosproblems.com/376

theorem Erdos376.erdos_376 : {n : ℕ | n.centralBinom.Coprime 105}.Infinite ↔ sorry

Are there infinitely many $n$ such that ${2n\choose n}$ is coprime to $105$?

theorem Erdos376.erdos_376.variants.prime {p q : ℕ} (h₁ : Nat.Prime p) (h₂ : Odd p) (h₃ : Nat.Prime q) (h₄ : Odd q) : {n : ℕ | n.centralBinom.Coprime (p * q)}.Infinite

Erdős, Graham, Ruzsa, and Straus [EGRS75] have shown that, for any two odd primes $p$ and $q$, there are infinite many $n$ such that ${2n\choose n}$ is coprime to $pq$.