Formal target: Corpus.OEIS48153.conjecture

"Conjecture: $a(n) <= \frac{n^2-1}{2}$.

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 1 n →
    LE.le.{0} (Corpus.OEIS48153.a n) (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} n 2) 1) 2)

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

Environment availability: available.