Formal target: Corpus.OEIS7918.conjecture1

According to the "k-tuple" conjecture, $a(n)$ is the initial term of the lexicographically earliest increasing arithmetic progression of $n$ primes; the corresponding common differences are given by A061558.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    Eq.{1} (Corpus.OEIS7918.a n)
      (InfSet.sInf.{0} (Set.ofPred.{0} fun p0 => Exists.{1} fun d => Corpus.OEIS7918.isApOfNPrimes n p0 d))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record