Formal target: Corpus.OEIS22030.conjecture

Conjecture: $a(n) = 4 a(n-1) - a(n-3) + a(n-4)$.

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 4 n →
    Eq.{1} (Corpus.OEIS22030.a n)
      (HAdd.hAdd.{0, 0, 0}
        (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} 4 (Corpus.OEIS22030.a (HSub.hSub.{0, 0, 0} n 1)))
          (Corpus.OEIS22030.a (HSub.hSub.{0, 0, 0} n 3)))
        (Corpus.OEIS22030.a (HSub.hSub.{0, 0, 0} n 4)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record