Formal target: Corpus.OEIS117545.conjecture

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

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    Exists.{1} fun k =>
      And (GT.gt.{0} k 0) (Nat.Prime (Polynomial.eval.{0} (Nat.cast.{0} n) (Polynomial.cyclotomic.{0} k Int)).natAbs)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record