Formal target: Corpus.OEIS80101.conjecture

It is conjectured that $a(n) \le 2$ for all $n$.

Exact formal statement

∀ (n : Nat), LE.le.{0} (Corpus.OEIS80101.a n) 2

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

Environment availability: available.