Formal target: Corpus.OEIS228828.conjecture
Conjecture: the sequence A228828 is infinite.
Exact formal statement
Set.Infinite.{0} (Set.ofPred.{0} fun x => Exists.{1} fun n => Eq.{1} (Corpus.OEIS228828.a n) x)This target is a formal statement, not a proof of the problem.
Environment availability: available.