Computer Search Settles 90-Year-Old Math Problem

A team of mathematicians has finally finished off Keller’s conjecture, but not by working it out themselves. Instead, they taught a fleet of computers to do it for them.

Keller’s conjecture, posed 90 years ago by Ott-Heinrich Keller, is a problem about covering spaces with identical tiles. It asserts that if you cover a two-dimensional space with two-dimensional square tiles, at least two of the tiles must share an edge. It makes the same prediction for spaces of every dimension — that in covering, say, 12-dimensional space using 12-dimensional “square” tiles, you will end up with at least two tiles that abut each other exactly.

Over the years, mathematicians have chipped away at the conjecture, proving it true for some dimensions and false for others. As of this past fall the question remained unresolved only for seven-dimensional space.

But a new computer-generated proof has finally resolved the problem. The proof, posted online last October, is the latest example of how human ingenuity, combined with raw computing power, can answer some of the most vexing problems in mathematics. 

The authors of the new work — Joshua Brakensiek of Stanford University, Marijn Heule and John Mackey of Carnegie Mellon University, and David Narváez of the Rochester Institute of Technology — solved the problem using 40 computers. After a mere 30 minutes, the machines produced a one-word answer: Yes, the conjecture is true in seven dimensions. And we don’t have to take their conclusion on faith.

The answer comes packaged with a long proof explaining why it’s right. The argument is too sprawling to be understood by human beings, but it can be verified by a separate computer program as correct.

In other words, even if we don’t know what the computers did to solve Keller’s conjecture, we can assure ourselves they did it correctly.

The Mysterious Seventh Dimension

It’s easy to see that Keller’s conjecture is true in two-dimensional space. Take a piece of paper and try to cover it with equal-sized squares, with no gaps between the squares and no overlapping. You won’t get far before you realize that at least two of the squares need to share an edge. If you have blocks lying around it’s similarly easy to see that the conjecture is true in three-dimensional space. In 1930, Keller conjectured that this relationship holds for corresponding spaces and tiles of any dimension.

Early results supported Keller’s prediction. In 1940, Oskar Perron proved that the conjecture is true for spaces in dimensions one through six. But more than 50 years later, a new generation of mathematicians found the first counterexample to the conjecture: Jeffrey Lagarias and Peter Shor proved that the conjecture is false in dimension 10 in 1992. 

A simple argument shows that once the conjecture is false in one dimension, it’s necessarily false in all higher dimensions. So after Lagarias and Shor, the only unsettled dimensions were seven, eight and nine. In 2002, Mackey proved Keller’s conjecture false in dimension eight (and therefore also in dimension nine).

That left just dimension seven open — it was either the highest dimension where the conjecture holds or the lowest dimension where it fails.

“Nobody knows exactly what’s going on there,” said Heule.

Connect the Dots

As mathematicians chipped away at the problem over the decades, their methods changed. Perron worked out the first six dimensions with pencil and paper, but by the 1990s, researchers had learned how to translate Keller’s conjecture into a completely different form — one that allowed them to apply computers to the problem.

The original formulation of Keller’s conjecture is about smooth, continuous space. Within that space, there are infinitely many ways of placing infinitely many tiles. But computers aren’t good at solving problems involving infinite options — to work their magic they need some kind of discrete, finite object to think about.

In 1990, Keresztély Corrádi and Sándor Szabó came up with just such a discrete object. They proved that you can ask questions about this object that are equivalent to Keller’s conjecture — so that if you prove something about these objects, you necessarily prove Keller’s conjecture as well. This effectively reduced a question about infinity to an easier problem about the arithmetic of a few numbers. 

Here’s how it works.

Say you want to solve Keller’s conjecture in dimension two. Corrádi and Szabó came up with a method for doing this by building what they called a Keller graph. 

To start, imagine 16 dice on a table, each positioned so that the face with two dots is facing up. (The fact that it’s two dots reflects the fact that you’re addressing the conjecture for dimension two; we’ll see why it’s 16 dice in a moment.) Now color each dot using any of four colors: red, green, white or black. 

The positions of dots on a single die are not interchangeable: Think of one position as representing an x-coordinate and the other as representing a y-coordinate. Once the dice are colored, we’ll start drawing lines, or edges, between pairs of dice if two conditions hold: The dice have dots in one position that are different colors, and in the other position they have dots whose colors are not only different but paired, with red and green forming one pair and black and white the other. 

So, for example, if one die has two red dots and the other has two black dots, they’re not connected: While they meet the criteria for one position (different colors), they don’t meet the criteria for the other (paired colors). However, if one die is colored red-black and the other is colored green-green they are connected, because they have paired colors in one position (red-green) and different colors in the other (black-green).

There are 16 possible ways of using four colors to color two dots (that’s why we’re working with 16 dice). Array all 16 possibilities in front of you. Connect all pairs of dice that fit the rule. Now for the crucial question: Can you find four dice that are all connected to each other?

Such fully connected subsets of dice are called a clique. If you can find one, you’ve proved Keller’s conjecture false in dimension two. But you can’t, because it won’t exist. The fact that there’s no clique of four dice means Keller’s conjecture is true in dimension two. 

The dice are not literally the tiles at issue in Keller’s conjecture, but you can think of each die as representing a tile. Think of the colors assigned to the dots as coordinates which situate the dice in space. And think of the existence of an edge as a description of how two dice are positioned relative to each other. 

If two dice have the exact same colors, they represent tiles that are in the exact same position in space. If they have no colors in common and no paired colors (one die is black-white and the other is green-red), they represent tiles that would partially overlap — which, remember, is not allowed in the tiling. If the two dice have one set of paired colors and one set of the same color (one is red-black and the other is green-black) they represent tiles that share a face. 

Finally, and most importantly, if they have one set of paired colors and another set of colors that are merely different — that is, if they’re connected by an edge — it means the dice represent tiles that are touching each other, but shifted off each other slightly, so that their faces don’t exactly align. This is the condition you really want to investigate. Dice that are connected by an edge represent tiles that are connected without sharing a face — exactly the kind of tiling arrangement needed to disprove Keller’s conjecture.

“They need to touch each other, but they can’t fully touch each other,” Heule said.

Scaling Up

Thirty years ago, Corrádi and Szabó proved that mathematicians can use this procedure to address Keller’s conjecture in any dimension by adjusting the parameters of the experiment. To prove Keller’s conjecture in three dimensions you might use 216 dice with three dots on a face, and maybe three pairs of colors (though there’s flexibility on this point). Then you’d look for eight dice (2³) among them that are fully connected to each other using the same two conditions we used before. 

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 co-planners wants to invite Kemba or Brad or both of them. Your other co-planner, 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).

A computer program that solves propositional logic statements like this is called a SAT solver, where “SAT” stands for “satisfiability.” It explores every combination of variables and produces a one-word answer: Either YES, there is a way to satisfy the formula, or NO, there’s not.

“You just decide whether each variable is true or false in a way to make the whole formula true, and if you can do it the formula is satisfiable, and if you can’t the formula is unsatisfiable,” said Thomas Hales of the University of Pittsburgh.

The question of whether it’s possible to find a clique of size 128 is a similar kind of problem. It can also be written as a propositional formula and plugged into a SAT solver. Start with a large number of dice with seven dots apiece and six possible colors. Can you color the dots such that 128 dice can be connected to each other according to the specified rules? In other words, is there a way of assigning colors that makes the clique possible?

The propositional formula that captures this question about cliques is quite long, containing 39,000 different variables. Each can be assigned one of two values (0 or 1). As a result, the number of possible permutations of variables, or ways of arranging colors on the dice, is 2^39,000 — a very, very big number.

To answer Keller’s conjecture for dimension seven, a computer would have to check every one of those combinations — either ruling them all out (meaning no clique of size 128 exists, and Keller is true in dimension seven) or finding just one that works (meaning Keller is false). 

“If you had a naive computer check all possible [configurations], it would be this 324-digit number of cases,” Mackey said. It would take the world’s fastest computers until the end of time before they’d exhausted all the possibilities. 

But the authors of the new work figured out how computers could arrive at a definitive conclusion without actually having to check every possibility. Efficiency is the key.

Hidden Efficiencies

Mackey recalls the day when, in his eyes, the project really came together. He was standing in front of a blackboard in his office at Carnegie Mellon University discussing the problem with two of his co-authors, Heule and Brakensiek, when Heule suggested a way of structuring the search so that it could be completed in a reasonable amount of time.

“There was real intellectual genius at work there in my office that day,” Mackey said. “It was like watching Wayne Gretzky, like watching LeBron James in the NBA Finals. I have goose bumps right now [just thinking about it].”

There are many ways you might grease the search for a particular Keller graph. Imagine that you have many dice on a table and you’re trying to arrange 128 of them in a way that satisfies the rules of a Keller graph. Maybe you arrange 12 of them correctly, but you can’t find a way to add the next die. At that point, you can rule out all the configurations of 128 dice that involve that unworkable starting configuration of 12 tiles.

“If you know the first five things you’ve assigned don’t fit together, you don’t have to look at any of the other variables, and that generally cuts the search down a whole lot,” said Shor, who is now at the Massachusetts Institute of Technology.

Another form of efficiency involves symmetry. When objects are symmetric, we think of them as being in some sense the same. This sameness allows you to understand an entire object just by studying a portion of it: Glimpse half a human face and you can reconstruct the whole visage.

Similar shortcuts work for Keller graphs. Imagine, again, that you’re arranging dice on a table. Maybe you start at the center of the table and build out a configuration to the left. You lay four dice, then hit a roadblock. Now you’ve ruled out one starting configuration — and all configurations based on it. But you can also rule out the mirror image of that starting configuration — the arrangement of dice you get when you position the dice the same way, but building out to the right instead.

“If you can find a way of doing satisfiability problems that takes into account the symmetries in an intelligent way, then you’ve made the problem much easier,” said Hales.

The four collaborators took advantage of these kinds of search efficiencies in a new way — in particular, they automated considerations about symmetries, where previous work had relied on mathematicians working practically by hand to deal with them. 

They ultimately streamlined the search for a clique of size 128 so that instead of checking 2^39,000 configurations, their SAT solver only had to search about 1 billion (2³⁰). This turned a search that might have taken eons into a morning chore. Finally, after just half an hour of computations, they had an answer.

“The computers said no, so we know the conjecture does hold,” said Heule. There is no way of coloring 128 dice so that they’re all connected to each other, so Keller’s conjecture is true in dimension seven: Any arrangement of tiles that covers the space inevitably includes at least two tiles that share a face.

The computers actually delivered a lot more than a one-word answer. They supported it with a long proof — 200 gigabytes in size — justifying their conclusion.

The proof is much more than a readout of all the configurations of variables the computers checked. It’s a logical argument which establishes that the desired clique couldn’t possibly exist. The four researchers fed the Keller proof into a formal proof checker — a computer program that traced the logic of the argument — and confirmed it works. 

“You don’t just go through all the cases and not find anything, you go through all the cases and you’re able to write a proof that this thing doesn’t exist,” Mackey said. “You’re able to write a proof of unsatisfiability.”

This article was reprinted on Wired.com.