Formal target: Corpus.OEIS119591.conjecture

Is $a(n)$ defined for all $n \ge 2$?

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 2 n →
    Exists.{1} fun k =>
      And (GT.gt.{0} k 0) (Nat.Prime (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 (HPow.hPow.{0, 0, 0} n 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