The excluded grid theorem states that, for each positive integer 
, sufficiently large treewidth
forces a 
grid graph as a graph minor
(Robertson and Seymour 1984). Equivalently, graphs excluding
a fixed grid graph as a graph
minor have bounded treewidth. A minor model consists
of disjoint connected branch sets, with the required grid adjacencies represented
by edges between the corresponding branch sets.
Hajiaghayi (2026) reports absolute constants 
such that
 |
forces a 
grid graph minor for every integer 
. Under this promise, a randomized algorithm
constructs and checks a minor model in 
time with probability
at least 
, where the exponent is absolute and 
denotes big-O notation.
Independent repetition until a verified model is found has expected polynomial
time on inputs satisfying the promise. No such termination guarantee is asserted
for inputs that fail it.
Hajiaghayi (2026) reports AI assistance with mathematical ideas and arguments and a companion Lean formalization using explicit interfaces for earlier algorithms. The bound does not settle the conjectured smaller exponents.
