Congruences of binomial sums Let $a_n$ is a binomial sum, for example
$$
a_n := \sum_{k} \binom{n-k}{k} \quad \text{or} \quad \sum_{k=0}^n\binom{n+k}{n-k}\binom{2k}{k}
\quad \text{or} \quad \sum_{k=0}^n\sum_{\ell=0}^k\binom{n}{k}\binom{n+k}{k}\binom{k}{\ell}^3
$$
These are Fibonacci, Delannoy and Apéry numbers. More generally, we can consider
the sequence $\{a_n\}$ obtained as a diagonal of a rational function over $\Bbb Z$ (so in particular it is P-recursive), see e.g. Stanley, "Enumerative Combinatorics", Chapter 6.
Question: Given $m\in \Bbb N$ and a binomial sum $\{a_n\}$, is it decidable whether $m$ divides $a_n$ for all $n\in \Bbb N$?
This might seem a bit naive, and I supect this should be true, but couldn't find the reference.  Note the Skolem's Problem which is different but has a similar flavor (and not known to be decidable).
 A: I found the reference:  Theorem 9.1 in Boris Adamczewski and Jason P. Bell, Diagonalization and Rationalization of algebraic Laurent series, Ann. Sci. Éc. Norm. Supér. 46 (2013), 963–1004.
The authors even discuss the Apéry sequence modulo 5, right after the theorem.
It's sort of amazing when the reference request works out so well.  I thank Boris Adamczewski and Jason Bell for telling me about this remarkable work.
A: These binomial sequences, and diagonals, are holonomic, meaning that they satisfy recurrence relations with polynomial coefficients.
If the leading coefficient has no roots modulo m, then the question becomes easy.
But I guess that in many situations, this polynomial does have roots modulo m.
If one can find a closed form expression for the generating function of such the sequence, then that can also be a way for proving that the sequence (divided by m) is an integer sequence.
I don't know of any holonomic sequence with integer terms for which there is no known formula that proves that the terms are integers (an integer-but-not-proven-integer holonomic sequence).
But a general decision procedure to prove/disprove that a holonomic sequence (divided by m) has integer entries, I don't think that is known.
