Formal target: Corpus.WikipediaWoodalPrimes.infinitely_many_woodall_primes

There are infinitely many prime numbers of the form k * 2 ^ k - 1 for k > 1.

Exact formal statement

Set.Infinite.{0}
  (Set.ofPred.{0} fun k =>
    And (LT.lt.{0} 1 k) (Nat.Prime (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} k (HPow.hPow.{0, 0, 0} 2 k)) 1)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record