An example of proving summation identities with computer

I am trying to learn how to use computers to prove identities like this one

$$ \sum_{k=m}^n{k\choose k-m}{2n\choose 2k}=4^{n-m}\frac{n(2n-m-1)!}{(2n-2m)!m!}, $$

which I came across on math.stackexchange.com. If you put it Mathematica and simplify, you will simply get a True without any explanation. But how dose computer know it? In the following, I will explain one possible way that machines can prove this for us -- using creative telescoping algorithms.

I am going to use the Mathematica package Sigma by Carsten Schneider.

First the left-hand-side can be written as

$$ S(n_0)=\underset{k=0}{\overset{n_0}{\sum }} f(n_0,k) $$

where $n_0=n-m$ and

$$ f(n_0,k)= \left( \begin{array}{c} k+m \\ k \\ \end{array} \right) \left( \begin{array}{c} 2 \left(m+n_0\right) \\ 2 (k+m) \\ \end{array} \right) . $$

Next, let

$$ c_0(n)=2 (1 + m + n_0) (m + 2 n_0) (1 + m + 2 n_0), $$

and

$$ c_1(n)=-(1 + n_0) (m + n_0) (1 + 2 n_0) $$

and

$$ g(n_0,k)=-\frac{k (2 k+2 m-1) \left(m+n_0+1\right) \binom{k+m}{k} \left(2 k m+4 k n_0+2 k-4 m n_0-3 m-6 n_0^2-7 n_0-2\right) \binom{2 m+2 n_0}{2 k+2 m}}{\left(2 k-2 n_0-1\right) \left(k-n_0-1\right)}. $$

Then you can verify in your favorite CAS system that

$$ g\left(n_0,k+1\right)-g\left(n_0,k\right)=c_0\left(n_0\right) f\left(n_0,k\right)+c_1\left(n_0\right) f\left(n_0+1,k\right) . $$

I did not magically find this recursion myself. This is done by Sigma.

Summing over $k=1,..n_0-1$, the left-hand-side telescopes (perhaps this is where the name creative-telescoping comes from), and we get

$$ c_0(n_0) S\left(n_0\right)+c_1(n_0) S\left(n_0+1\right)=0 $$

This is a simple recursion. Put in $S(0)=f(0,0)=1$, we get

$$ S(n_0)= \frac{4^{n_0} \left(m+n_0\right) \left(m+2 n_0-1\right)!}{m! \left(2 n_0\right)!} = \frac{n 4^{n-m} (-m+2 n-1)!}{m! (2 n-2 m)!} . $$

where we substitute by $n_0=n-m$. This is exactly the right-hand-side.

All these have been completely automated. What you need to do is only to trust the computer when it says something is true. See Schneider's paper for many more examples!