The Resolution of Keller's Conjecture

TL;DR

This paper proves Keller's conjecture is true in 7 dimensions by showing no large clique exists in related graphs, using automated SAT solving techniques, and confirms the existence of a faceshare-free tiling in 8 dimensions.

Contribution

The paper introduces an automated SAT-based method to resolve Keller's conjecture in dimension 7, providing a complete proof of the conjecture's truth in this case.

Findings

No clique of size 128 exists in the graphs related to Keller's conjecture in dimension 7.

Every unit cube tiling in -dimensional space contains a facesharing pair.

A faceshare-free tiling exists in 8 dimensions, confirming the conjecture's boundary.

Abstract

We consider three graphs, $G_{7,3}$, $G_{7,4}$, and $G_{7,6}$, related to Keller's conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size $2^7 = 128$. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling of $\mathbb{R}^7$ contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of $\mathbb{R}^8$ exists (which we also verify), this completely resolves Keller's conjecture.