*September 28, 2020*

# Last remaining case of Keller's conjecture resolved with computer-assisted proof

It is not hard to see that any tiling of the plane with squares must include pairs of squares that share a full edge. (Here a tiling is a collection of squares that cover the full plane with the property that that interiors of the squares do not intersect.) It is also not hard to see that any tiling of three-dimensional space with cubes includes cubes that intersect in a full two-dimensional face. On this front, Ott-Heinrich Keller conjectured in 1930 that the analogous result holds in any dimension. This has been confirmed up to dimension 6, but it is known to be false in dimension 8 or more. (The latter result is due to our own John Mackey, who improved a previous result of Jeff Lagarias and Peter Shor.) Thus, the last remaining open case for Keller's conjecture was the 7-dimensional case. This has been the status of the problem for several years.

However, this question was recently resolved by John Mackey in joint work with CMU alum Josh Brakensiek (who was a Knaster-McWilliams scholar and is now in the CS PhD program at Stanford), Marijn Heule of the CMU Computer Science Department, and David Narvaez of RIT. A carefully constructed computer search is a key component of the proof. For more on this result, see Marijn Heule's discussion. This work was also featured in Quanta.