Proof of Ira Gessel's Lattice Path Conjecture

TL;DR

This paper provides a computer-aided, fully rigorous proof of Gessel's lattice path conjecture, which counts specific constrained walks on the square lattice with a closed-form formula.

Contribution

It introduces a novel computer-assisted proof technique to rigorously verify Gessel's conjecture on lattice paths.

Findings

Confirmed Gessel's conjecture with a rigorous proof

Derived a closed-form enumeration formula for the constrained walks

Demonstrated the effectiveness of computer-aided proofs in combinatorics

Abstract

We present a computer-aided, yet fully rigorous, proof of Ira Gessel's tantalizingly simply-stated conjecture that the number of ways of walking $2n$ steps in the region $x+y \geq 0, y \geq 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\frac{(5/6)_n(1/2)_n}{(5/3)_n(2)_n}$ .