In a recent article, Manuel Kauers and I tried very hard to prove Ira Gessel's notorious conjecture, that has been circulating in combinatorial enumeration circles for the last seven years, about the number of ways of walking, in the "Manhattan lattice" (2D square-lattice), 2n steps, from the origin back to the origin, using unit steps in the four fundamental directions (north, south, east, and west), all the while staying in x+y ≥ 0, y ≥ 0. Ira Gessel conjectured that it is given by the beautiful expression
[ 16ⁿ (5/6)_n (1/2)_n]/[(5/3)_n (2)_n]   , where   (a)_n=a(a+1)...(a+n-1)   .
We failed, becuase our computers ran out of memory, even though we felt that a sufficiently large computer would yield to our approach. But then came along the brilliant Christoph Koutschan, and joined the effort, and together with Manuel, was able to complete the task, still using our ideas, but adding to them some very good ones of his own, and this lead to the final solution.

• The Maple file Guessel1 that has the annihilating operator described in the paper, and the input to the checking procedure, bdok(n), is numeric n, and that verifies that Gessel's expression does indeed satisfy it numerically for n from 0 to 205. Note that this is already a rigorous proof, since the calculation boils down to proving that a certain polynomial of degree ≤ 205 is identically zero. To use it, download it into a directory, and type (in Linux)
  maple -q < Guessel1
  and you should get the following output
• The Maple file Guessel2 that has the annihilating operator described in the paper, and the checking procedure, bdok1(n); now takes symbolic input. It verifies, this time symbolically, that Gessel's expression does indeed satisfy it (for symbolic n, and hence, in particular for all integer n). To run it, download it into a directory, and type
  maple -q < Guessel2
  and you should get the following output.
• There is still one minor technicality. The homog. linear recurrence equation, of order 32, may, a priori, be "singular", i.e. have positive integer roots. In that case, we would have to check more than the first 32 initial values. If K is the largest positive integer root of the coeff. of f(n+32) in the recurrence equation, let's call it P₀(n), then we would have to check the first max(32,32+K) initial values. Fortunately, when Maple factors P₀(n) you only get factors of the form (an+b), with a and b positive integers, as well as other higher-degree factors. So K=-infinity, and 32 initial values suffice. Here is the Maple file, GuesselP0, that factors the leading coeff. P₀(n). To run it, download it into a directory, and type
  maple -q < GuesselP0
  and you should get the following output.
• But how did we come up with this order-32, degree-172, linear-recurrence-with-polynomial-coefficients annihilating operator Monster? We could have easily cheated and cooked it up by taking the minimal operator of order 2, satisfied by the conjectured expression, and left-multiplied it by a random monstrous order-30 operator with gigantic coefficients, and pretented that it came out from our non-commutative Groebner bases program. For those who have any suspicion, here is Christoph Koutschan's Mathematica Notebook, that describes all the needed steps, and that would enable the skeptic (and patient!) reader to check all the steps.
• Finally, the set of 16 annihilating operators that formed the basis for the elimination described in the article is the set S given right here.

Doron Zeilberger's Home Page