Formal target: Corpus.OEIS2407.conjecture
This sequence is believed to be infinite.
Exact formal statement
Set.Infinite.{0} (Set.ofPred.{0} fun p => Corpus.OEIS2407.A p)This target is a formal statement, not a proof of the problem.
Environment availability: available.