Formal target: Corpus.OEIS117531.conjecture

Conjecture: $a(n) < n$ for $n > 13$.

Exact formal statement

∀ (n : Nat), GT.gt.{0} n 13 → LT.lt.{0} (Corpus.OEIS117531.a n) n

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

Environment availability: available.