The problem
Claim: in every tiling of \mathbb{R}^n by congruent unit cubes (edges parallel not required), some two cubes share a complete (n−1)-dimensional face.
Keller's Conjecture
historicReferences
History & significance
True for n ≤ 6 (Perron 1940). False for n ≥ 8: Lagarias and Shor (1992) built counterexamples via dissection methods, Mackey simplified to dimension 8 (2002), implying all higher. Only dimension 7 survived, resisting both geometric and computational assault for thirty years.
The resolution (computer-assisted proof)
Closed August 2020 by Brakensiek, Heule, Mackey and Narváez: the n = 7 case was reduced to finitely many clique problems on a quotient graph (via the Keller graph machinery of Mackey), discharged by the Clasp SAT solver, with the solver's answer independently verified in the Lean proof assistant — a template for trustworthy extreme-scale discrete proof. With dimension 7 negative, Keller's conjecture is false in every dimension ≥ 7: a 90-year-old geometric intuition, fully mapped.