Formal target: Corpus.OEIS185895.conjecture1

$a(n)$ differs in sign from $a(n-1)$ if and only if $n$ is a triangular number (checked up to $n = 1225 = (50 \cdot 51)/2$).

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    Iff (LT.lt.{0} (HMul.hMul.{0, 0, 0} (Corpus.OEIS185895.a n) (Corpus.OEIS185895.a (HSub.hSub.{0, 0, 0} n 1))) 0)
      (Corpus.OEIS185895.IsTriangular n)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record