Proof of Ira Gessel's lattice path conjecture

We present a computer-aided, yet fully rigorous, proof of Ira Gessel's tantalizingly simply stated conjecture that the number of ways of walking 2 n steps in the region x + y ≥ 0, y ≥ 0 of the square lattice with unit steps in the east, west, north, and south directions, that start and end at the origin, equals 16 n ( 5 / 6 ) n ( 1 / 2 ) n ( 5 / 3 ) n ( 2 ) n .