Formal target: Corpus.Erdos891.erdos_891.variants.weisenberg

Weisenberg has observed that Dickson's conjecture implies the answer is no if we replace $p_1\cdots p_k$ with $p_1\cdots p_k-1$.

Exact formal statement

∀ (k : Nat),
  GE.ge.{0} k 2 →
    Filter.Frequently.{0}
      (fun n =>
        ∀ (m : Nat),
          Membership.mem.{0, 0}
              (Finset.Ico.{0} n
                (HSub.hSub.{0, 0, 0}
                  (HAdd.hAdd.{0, 0, 0} n (Finset.prod.{0, 0} (Finset.range k) fun i => Nat.nth Nat.Prime i)) 1))
              m →
            LE.le.{0} (DFunLike.coe.{1, 1, 1} ArithmeticFunction.cardDistinctFactors m) k)
      Filter.atTop.{0}

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record