Formal target: Corpus.OEIS53175.conjecture

Conjecture: let $P(n)$ be the $(n+1) \times (n+1)$ Hankel-type determinant with $(i,j)$-entry equal to $a(i+j)$ for all $i,j = 0, \ldots, n$.

Exact formal statement

∀ (n : Nat),
  have detP := Matrix.det.{0, 0} (Corpus.OEIS53175.hankelMatrix n);
  have pow2 := HPow.hPow.{0, 0, 0} 2 (HMul.hMul.{0, 0, 0} n (HAdd.hAdd.{0, 0, 0} n 3));
  And (Dvd.dvd.{0} pow2 detP)
    (And (LT.lt.{0} 0 (HDiv.hDiv.{0, 0, 0} detP pow2))
      (Eq.{1} (HMod.hMod.{0, 0, 0} (HDiv.hDiv.{0, 0, 0} detP pow2) 2) 1))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record