Formal target: Corpus.OEIS34694.conjecture

"Conjecture: $a(n) < n^2$ for $n > 1$.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 1 n → LT.lt.{0} (Corpus.OEIS34694.a n) (HPow.hPow.{0, 0, 0} n 2)

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

Environment availability: available.