Formal target: Corpus.Arxiv11041579CunninghamChain.infinitely_many_firstKind_chains

Jones's conjecture (first kind): for every positive integer $k$, there are infinitely many primes $p$ that start a first-kind Cunningham chain of exactly length $k$.

Exact formal statement

∀ (k : Nat),
  LT.lt.{0} 0 k →
    Set.Infinite.{0} (Set.ofPred.{0} fun p => Corpus.Arxiv11041579CunninghamChain.IsFirstKindChainOfLength p k)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record