1. FormalConjectures
  2. ErdosProblems
  3. «931»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 931

Reference: erdosproblems.com/931

namespace Erdos931

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?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_931 : answer(sorry) ↔ ∀ᵉ (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 := ⊢ True ↔ ∀ (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 All goals completed! 🐙

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.

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_931.variants.additional_condition : answer(sorry) ↔ ∀ᵉ (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 := ⊢ True ↔ ∀ (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 All goals completed! 🐙

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

@[category research solved, AMS 11] theorem erdos_931.variants.additional_condition_nonempty : ∃ (k₁ k₂ : ℕ), ∃ (_h₁ : k₂ ≤ k₁), ∃ (_h₂ : 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 := ⊢ ∃ 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 use 10, 3, (⊢ 3 ≤ 10 All goals completed! 🐙), (⊢ 3 ≤ 3 All goals completed! 🐙) ⊢ (0, 13) ∈ {(n₁, n₂) | n₁ + 10 ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + 10) ∧ (∏ i ∈ Finset.Icc 1 10, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 3, (n₂ + j)).primeFactors} ⊢ Nat.primeFactors 3628800 = Nat.primeFactors 3360 All goals completed! 🐙

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$.

@[category research open, AMS 11] theorem declaration uses 'sorry'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 : ℕ), p.Prime ∧ n₁ ≤ p ∧ p ≤ n₂ := 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₂ All goals completed! 🐙 end Erdos931