A team of researchers has completed the understanding of the Keller Conjecture, first proposed in 1930, about the packing of squares, cubes, and their higher-dimensional analogues. The conjecture states that any tiling of identical hypercubes that fills space must contain a pair of neighbors that share an entire face.
You might convince yourself it is true for two or three dimensions by toying with squares or blocks. Mathematicians later established the status of the conjecture for all dimensions except seven. The new result, which shared the best paper award at the 2020 International Joint Conference on Automated Reasoning (IJCAR 2020), fills that gap. To do this, the researchers mapped more than 10,324 ways seven-dimensional hypercubes can avoid sharing any six-dimensional face onto a satisfiability problem, which asks whether some Boolean formula can ever be made true.