Formal target: Corpus.OEIS119563.conjecture
The first 5 entries are primes.
Exact formal statement
Set.Infinite.{0} (Set.ofPred.{0} fun n => Nat.Prime (Corpus.OEIS119563.a n))This target is a formal statement, not a proof of the problem.
Environment availability: available.