Formal target: Corpus.PaperPrimeTuples.prime_tuples_conjecture

For any k ≥ 2, let a₁,...,aₖ and b₁,...,bₖ be integers with aᵢ > 0.

Exact formal statement

∀ {k : Nat},
  LE.le.{0} 2 k →
    ∀ (a : Fin k → PNat) (b : Fin k → Nat),
      (∀ (p : Nat),
          Nat.Prime p →
            Exists.{1} fun n =>
              Not
                (Dvd.dvd.{0} p
                  (Finset.prod.{0, 0} Finset.univ.{0} fun i =>
                    HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} (a i).val n) (b i)))) →
        Set.Infinite.{0}
          (Set.ofPred.{0} fun n =>
            ∀ (i : Fin k), Nat.Prime (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} (a i).val n) (b i)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record