Some questions concerning computer-generated proofs of a binomial double- sum identity
In 1990 D. Zeilberger asked for a computer-generated proof of the following identity: \[ \sum^n_{i = 0} \sum^n_{j = 0} {i + j \choose j}^2 {4n - 2i - 2j \choose 2n - 2j} = (2n + 1) {2n \choose n}^2. \] The authors give two different proofs. The human part of the first proof consists in using a somehow tricky generating function argument. The rest is done by Zeilberger's algorithm in the implementation of \textit{D. Zeilberger} himself for Maple [SIGSAM Bull. 25, 4-13 (1991)] or in that of \textit{P. Paule} and \textit{M. Schorn} for Mathematica (to appear). The second proof is by observing that a generalization of the left hand side of the above formula satisfies a simple structured recurrence relation. This generalization was obtained by an heuristic process using any computer-algebra package. The authors remark that hypergeometric methods seemingly do not succeed.
scientific article; zbMATH DE number 627597