formal-conjectures · oeis · ams-11
The sequence is given by the combinatorial identity:
$a(n) = \sum_{k = 0}^n \binom{n}{k} \binom{2n+k-1}{n-1}$
with $a(0) = 1$.
The recurrence given below can be rewritten in the form
$$(2n+1)(2n+2)P(2,n)a(n+1) - (2n-1)(2n-2)P(2,-n)a(n-1) = Q(2,n^2)a(n),$$
where the polynomial $Q(2,n) = 4(55n^2 - 34n + 3)$ and the polynomial $P(2,n) = 5n^2 - 5n + 1$
satisfies the symmetry condition $P(2,n) = P(2,1-n)$ and has real zeros.
More generally, for fixed $m = 1,2,3, \ldots$, we conjecture that the sequence $b(n) := a(mn)$
satisfies a recurrence of the form
$$( \prod_{k = 1}^{2m} (2mn + k) )P(2m,n)b(n+1) + (-1)^m( \prod_{k = 1}^{2*m} (2mn - k) )
P(2m,-n)b(n-1) = Q(2m,n^2)b(n),$$
where the polynomials $P(2m,n)$ and $Q(2m,n)$ have degree $2m$. Conjecturally, the polynomial
$P(2m,n) = P(2m,1-n)$ and has real zeros in the interval [0, 1].
The $4m$ zeros of the polynomial $Q(2m,n^2)$ seem to belong to the interval $[-1, 1]$ and
$4m - 2$ of these zeros appear to be approximated by the rational numbers
$\pm k/(3m)$, where $1 \le k \le 3m - 2$, $k$ not a multiple of $3$.
Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://oeis.org/A103885
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/OEIS/103885.lean
Local target: Corpus.OEIS103885.conjecture
Source SHA-256: 1a199b5163eec7ca1ca37b1ebf3841d18725cbff30ec3519cd0d69fb061af205
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
The recurrence given below can be rewritten in the form $$(2n+1)(2n+2)P(2,n)a(n+1) - (2n-1)(2n-2)P(2,-n)a(n-1) = Q(2,n^2)a(n),$$ where the polynomial $Q(2,n) = 4(55n^2 - 34n + 3)$ and the polynomial $P(2,n) = 5n^2 - 5n + 1$ satisfies the symmetry condition $P(2,n) = P(2,1-n)$ and
No public records on this page.
No public records on this page.