Formal target: Corpus.OEIS64169.conjecture

"Conjecture: for $n > 2$, $n$ divides $a(n-2)$ if and only if $n$ is a prime.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 2 n → Iff (Dvd.dvd.{0} (Nat.cast.{0} n) (Corpus.OEIS64169.a (HSub.hSub.{0, 0, 0} n 2))) (Nat.Prime n)

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

Environment availability: available.