# The Resolution of Keller's Conjecture

arXiv: https://arxiv.org/abs/1910.03740 · HTML: https://mlsanity.com/paper/1910.03740/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Oct 2019.

## Built on by (most cited first, 8 of 8)

- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [Too much information: why CDCL solvers need to forget learned clauses](https://mlsanity.com/paper/2202.01030/) (2022)
- [Design of quantum optical experiments with logic artificial intelligence](https://mlsanity.com/paper/2109.13273/) (2021)
- [Inverting Cryptographic Hash Functions via Cube-and-Conquer](https://mlsanity.com/paper/2212.02405/) (2022)
- [SAT-based Circuit Local Improvement](https://mlsanity.com/paper/2102.12579/) (2021)
- [A short review on the maximum clique problem algorithms with classical, AI, and quantum methods](https://mlsanity.com/paper/2403.09742/) (2024)
- [Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery](https://mlsanity.com/paper/2604.21187/) (2026)
- [Streaming LRAT Certificates into Lean Theorems](https://mlsanity.com/paper/2607.00815/) (2026)

## Abstract (arXiv)

We consider three graphs, G7,3, G7,4, and G7,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 27 = 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 ℝ7 contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of ℝ8 exists (which we also verify), this completely resolves Keller's conjecture.