组合序列部分和同余定理的自动发现与证明

许多组合序列（例如 Catalan 数和 Motzkin 数）可表示为某些含整数系数的变量 $x$ 的 Laurent 多项式 $P(x)$ 和 $Q(x)$ 的 $P(x)^k Q(x)$ 的常数项。将此类序列记为 $a_k$，我们得到一个通用公式，可将不定和 $\sum_{k=0}^{rp -1} a_k$ 模 $p$ 的同余类（对于任意素数 $p$ 和任意正整数 $r$）确定为满足常系数线性递推（即差分）方程的序列的线性组合。这使我们（或更准确地说，我们的计算机）能够自动发现并证明此类部分和的同余定理。此外，我们证明在许多情况下，无论素数 $p$ 如何，剩余类的集合都是有限的。