Formal target: Corpus.OEIS87571.conjecture
Conjecture: There are infinitely many composite numbers $n$ such that $a(n)$ is nonzero.
Exact formal statement
∀ (M : Nat),
Exists.{1} fun n =>
And (GT.gt.{0} n M) (And (LT.lt.{0} 1 n) (And (Not (Nat.Prime n)) (Ne.{1} (Corpus.OEIS87571.a n) 0)))This target is a formal statement, not a proof of the problem.
Environment availability: available.