Keller's conjecture

Solved in 2020 by Joshua Brakensiek, Marijn Heule, John Mackey and David Narváez.

Oskar Perron proved the conjecture in dimensions up to 6 in 1940. In 1992 Jeffrey Lagarias and Peter Shor disproved it in dimension 10 by finding a large clique in the associated Keller graph, and John Mackey extended the failure down to dimension 8 in 2002. That left only dimension 7. Brakensiek, Heule, Mackey and Narváez encoded the remaining case as a satisfiability problem, used symmetry breaking to shrink the search, and showed with a SAT solver that no counterexample exists. Their 2020 result completes the answer, true for $n\le 7$ and false for $n\ge 8$.

References

• Keller's conjecture (Wikipedia)
• J. Brakensiek, M. Heule, J. Mackey, D. Narváez, The Resolution of Keller's Conjecture (arXiv:1910.03740)