Erdős Problem 730

Reference: erdosproblems.com/730

theorem 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 erdos_730.variants.explicit_pairs : {(87, 88), (607, 608)} ⊆ S✝

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

theorem erdos_730.variants.two_div_forall (n : ℕ) (h : 0 < n) : 2 ∣ (2 * n).choose n

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

theorem erdos_730.variants.succ_pair_criterion (n : ℕ) (h : 2 < n) : (n, n + 1) ∈ S✝ ↔ ∀ p ∈ Set.Ioc 2 n, ∀ [hp : Fact (Nat.Prime p)], let kummer_condition := fun (n : ℕ) => List.Forall (fun (m : ℕ) => m ≤ (p - 1) / 2) (p.digits n); kummer_condition n ↔ kummer_condition (n + 1)

Show that $(n, n+1) ∈ S$ if and only if for all odd primes $p ≤ n$ both the base $p$ representations of $n$ and $n+1$ either both have all digits less or equal to $(p-1)/2$ or both don't.

Note: currently there is stronger, but potentially false formulation of this criterion on erdosproblems.com.

theorem erdos_730.variants.succ_pair_growth : let C := fun (x : ℝ) => ↑(Finset.filter (fun (n : ℕ) => (n, n + 1) ∈ S✝) (Finset.Icc 0 ⌊x⌋₊)).card; Filter.Tendsto (fun (x : ℝ) => x / Real.log x ^ 2 / C x) Filter.atTop (nhds 0)

Standard heuristics then predict there should be $≫ \frac x {(\log x)^2}$ many $n ≤ x$ such that $(n, n+1) ∈ S$.