Abstract :
An algorithm for proving terminating hypergeometric identities, and thus binomial coefficients identities, is presented. It is based upon Gosperʹs algorithm for indefinite hypergeometric summation. A MAPLE program implementing this algorithm succeeded in proving almost all known identities. Hitherto the proof of such identities was an exclusively human endeavor.
