Erdős Problem 730

References:

• erdosproblems.com/730
• A129515

@[reducible, inline]

abbrev S : Set (ℕ × ℕ)

Equations

• S = {(n, m) : ℕ × ℕ | n < m ∧ n.centralBinom.primeFactors = m.centralBinom.primeFactors}

theorem Erdos730.erdos_730 : S.Infinite ↔ sorry

Are there infinitely many pairs of integers $n < m$ such that $\binom{2n}{n}$ and $\binom{2m}{m}$ have the same set of prime divisors?

theorem Erdos730.erdos_730.variants.explicit_pairs : {(87, 88), (607, 608)} ⊆ S

For example, $(87,88)$ and $(607,608)$ are such pairs.

theorem Erdos730.erdos_730.variants.two_div_forall (n : ℕ) (h : 0 < n) : 2 ∣ n.centralBinom

Show that for all $n$, the binomial coefficient $\binom{2n}{n}$ is even.

theorem Erdos730.erdos_730.variants.delta_ne_one : ∃ (n : ℕ) (m : ℕ), (n, m) ∈ S ∧ m ≠ n + 1

There are examples where $(n, m) ∈ S$ with $m ≠ n + 1$.

(Found by AlphaProof, although it was implicit already in [A129515])