Formal target: Corpus.Erdos931.erdos_931.variants.exists_prime

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

Exact formal statement

∀ (k₁ k₂ n₁ n₂ : Nat),
  LE.le.{0} k₂ k₁ →
    LE.le.{0} 3 k₂ →
      LE.le.{0} (HAdd.hAdd.{0, 0, 0} n₁ k₁) n₂ →
        Eq.{1} (Finset.prod.{0, 0} (Finset.Icc.{0} 1 k₁) fun i => HAdd.hAdd.{0, 0, 0} n₁ i).primeFactors
            (Finset.prod.{0, 0} (Finset.Icc.{0} 1 k₂) fun j => HAdd.hAdd.{0, 0, 0} n₂ j).primeFactors →
          Exists.{1} fun p => And (Nat.Prime p) (And (LE.le.{0} n₁ p) (LE.le.{0} p n₂))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record