Erdős Problem 931

Reference: erdosproblems.com/931

theorem erdos_931 : (∀ (k₁ k₂ : ℕ), k₂ ≥ 3 → k₂ ≤ k₁ → {(n₁, n₂) : ℕ × ℕ | n₁ + k₁ ≤ n₂ ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite) ↔ sorry

Let $k_1 \geq k_2 \geq 3$. Are there only finitely many $n_2\geq n_1 + k_1$ such that $$ \prod_{1\leq i\leq k_1}(n_1 + i)\ \text{and}\ \prod_{1\leq j\leq k_2} (n_2 + j) $$ have the same prime factors?

theorem erdos_931.variants.additional_condition : (∀ (k₁ k₂ : ℕ), k₂ ≥ 3 → k₂ ≤ k₁ → {(n₁, n₂) : ℕ × ℕ | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite) ↔ sorry

Erdős thought perhaps if the two products have the same factors then $n_2 > 2(n_1 + k_1)$. It is an open question whether this is true when allowing a finite number of counterexamples.

theorem erdos_931.variants.additional_condition_nonempty : ∃ (k₁ : ℕ) (k₂ : ℕ) (_ : k₂ ≤ k₁) (_ : 3 ≤ k₂), {(n₁, n₂) : ℕ × ℕ | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Nonempty

In fact there exist counterexamples, like this one found by AlphaProof.

theorem erdos_931.variants.exists_prime (k₁ k₂ n₁ n₂ : ℕ) (h₁ : k₂ ≤ k₁) (h₂ : 3 ≤ k₂) (h₃ : n₁ + k₁ ≤ n₂) (h₄ : (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors) : ∃ (p : ℕ), Nat.Prime p ∧ n₁ ≤ p ∧ p ≤ n₂

Erdős was unable to prove that if the two products have the same factors then there must exist a prime between $n_1$ and $n_2$.