Formal target: Corpus.OEIS93818.conjecture
Conjecture: Every odd prime occurs as a term in the sequence.
Exact formal statement
∀ (p : Nat), Nat.Prime p → Ne.{1} p 2 → Exists.{1} fun n => And (GT.gt.{0} n 0) (Eq.{1} (Corpus.OEIS93818.a n) p)This target is a formal statement, not a proof of the problem.
Environment availability: available.