For every integer n≥ 1 and every tiling T of R^n by unit n-dimensional cubes, there exist distinct cubes C,C'∈T such that C cap C' is a complete (n-1)-dimensional face of both C and C'.

Keller’s conjecture

Keller conjectured that every tiling of Euclidean space by equal unit cubes contains two cubes sharing an entire face. The conjecture was posed in 1930; its final unresolved case was settled by Brakensiek, Heule, Mackey, and Narváez in 2020.

Known results

Perron (1940) proved the conjecture in dimensions $n \le 6$ .
Lagarias and Shor (1992) constructed counterexamples in every dimension $n \ge 10$ .
Mackey (2002) extended the counterexamples to $n \ge 8$ .
Debroni, Eblen, Langston, Myrvold, Shor, and Weerapurage (2011) bounded the relevant seven-dimensional clique number by $124<2^7$ .

July 2026 end-to-end verification

Gallicchio, Codel, Avigad, and Heule formally verified the reduction, SAT encoding, symmetry arguments, solver certificates, and counterexample framework in Lean 4. This mechanically corroborates the established conclusion: the conjecture holds through dimension seven and fails from dimension eight onward; it is formalization, not a new resolution.

Current status (as of August 2026): Keller’s conjecture is resolved: it holds for $n \le 7$ and has counterexamples for $n \ge 8$ , with the complete known resolution now formally verified in Lean 4.

Keller’s conjecture

Primary source

Additional references

Progress summary

Solutions 0