As a general rule, to prove Keller’s conjecture in dimension n, you use dice with n dots and try to find a clique of size 2ⁿ. You can think of this clique as representing a kind of “super tile” (made up of 2ⁿ smaller tiles) that could cover the entire n-dimensional space.

So if you can find this super tile (that itself contains no face-sharing tiles), you can use translated, or shifted, copies of it to cover the entire space with tiles that don’t share a face, thus disproving Keller’s conjecture.

“If you succeed, you can cover the whole space by translation. The block with no common face will extend to the whole tiling,” said Lagarias, who is now at the University of Michigan.

Mackey disproved Keller’s conjecture in dimension eight by finding a clique of 256 dice (2⁸), so answering Keller’s conjecture for dimension seven required looking for a clique of 128 dice (2⁷). Find that clique, and you’ve proved Keller’s conjecture false in dimension seven. Prove that such a clique can’t exist, on the other hand, and you’ve proved the conjecture true.

Unfortunately, finding a clique of 128 dice is a particularly thorny problem. In previous work, researchers could use the fact that dimensions eight and 10 can be “factored,” in a sense, into lower-dimensional spaces that are easier to work with. No such luck here.

“Dimension seven is bad because it’s prime, which meant that you couldn’t split it into lower-dimensional things,” Lagarias said. “So there was no choice but to deal with the full combinatorics of these graphs.”

Seeking out a clique of size 128 may be a difficult task for the unassisted human brain, but it’s exactly the kind of question a computer is good at answering—especially if you give it a little help.

The Language of Logic

To turn the search for cliques into a problem that computers can grapple with, you need a representation of the problem that uses propositional logic. It’s a type of logical reasoning that incorporates a set of constraints.

Let’s say you and two friends are planning a party. The three of you are trying to put together the guest list, but you have somewhat competing interests. Maybe you want to either invite Avery or exclude Kemba. One of your coplanners wants to invite Kemba or Brad or both of them. Your other coplanner, with an ax to grind, wants to leave off Avery or Brad or both of them. Given these constraints, you could ask: Is there a guest list that satisfies all three party planners?

In computer science terms, this type of question is known as a satisfiability problem. You solve it by describing it in what’s called a propositional formula that in this case looks like this, where the letters A, K and B stand for the potential guests: (A OR NOT K) AND (K OR B) AND (NOT A OR NOT B).

The computer evaluates this formula by plugging in either 0 or 1 for each variable. A 0 means the variable is false, or turned off, and a 1 means it’s true, or turned on. So if you put in a 0 for “A” it means Avery is not invited, while a 1 means she is. There are lots of ways of assigning 1s and 0s to this simple formula—or building the guest list—and it’s possible that after running through them the computer will conclude it’s not possible to satisfy all the competing demands. In this case, though, there are two ways of assigning 1s and 0s that work for everyone: A = 1, K = 1, B = 0 (meaning inviting Avery and Kemba) and A = 0, K = 0, B = 1 (meaning inviting just Brad).