Formal target: Corpus.OEIS78729.conjecture

$(k+1)(k+2)(k+3)(k+4) + 1 = (k^2 + 5k + 5)^2$, which is never prime.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 0 n → Iff (Eq.{1} (Corpus.OEIS78729.a n) 0) (Eq.{1} n 4)

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

Environment availability: available.