Formal target: Corpus.OEIS109074.conjecture

It is conjectured that $\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right) = A005156(n+1)/A005156(n)$, where the OEIS comment reads A005156 as 1-based; with the 0-indexed b this is frac (n + 1) = b (n + 1) / b n.

Exact formal statement

∀ (n : Nat),
  Eq.{1} (Corpus.OEIS109074.frac (HAdd.hAdd.{0, 0, 0} n 1))
    (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS109074.b (HAdd.hAdd.{0, 0, 0} n 1)))
      (Nat.cast.{0} (Corpus.OEIS109074.b n)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record