Computer Search Settles 90-Year-Old Math Problem

Oct 5, 2020 | Location West County

Computer Search Settles 90-Year-Old Math Problem


Kevin Hartnett

Senior Writer

Ateam 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 2n. You can think of this clique as representing a kind of “super tile” (made up of 2n 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 (28), so answering Keller’s conjecture for dimension seven required looking for a clique of 128 dice (27). 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 239,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 239,000 configurations, their SAT solver only had to search about 1 billion (230). 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




Locations near
Ashburn 0.93 mi
43330 Junction Plaza
Ashburn, VA 20147
Sterling 4.07 mi
44 Pidgeon Hill Drive
Sterling, VA 20165
Leesburg 5.69 mi
521 E Market St
Leesburg, VA 20176
Herndon 7.66 mi
2465 Centreville Road
Herndon, VA 20171
Stone Ridge 7.88 mi
42020 Village Center Plaza
Stone Ridge, VA 20105
Reston 8.62 mi
1424 North Point Village Center
Reston, VA 20194
Purcellville 12.72 mi
1020 E Main St
Ste L
Purcellville, VA 20132
North Potomac 13.58 mi
12150 Darnestown Rd
Gaithersburg, MD 20878
Centreville 14.52 mi
5959 Centreville Crest Ln
Centreville, VA 20121
Fairfax 14.67 mi
11891 Grand Commons Ave
Fairfax, VA 22030
Potomac 14.98 mi
10232 River Road
Potomac, MD 20854
Germantown MD 15.03 mi
12800 Middlebrook Road
Germantown, MD 20874
Tysons 15.45 mi
328 Maple Ave E
Vienna, VA 22180
Haymarket 17.87 mi
15125 Washington St
Haymarket, VA 20169
Rockville 18.19 mi
20 Courthouse Square
Rockville, MD 20850
Mclean 18.23 mi
1320 Old Chain Bridge Road
Suite #190
McLean, VA 22101
Gaithersburg 18.71 mi
9132 Rothbury Drive
Gaithersburg, MD 20886
North Bethesda 20.42 mi
5268 Nicholson Ln
Kensington, MD 20895
Falls Church 20.59 mi
6674 Arlington Blvd
Falls Church, VA 22042
Manassas 20.65 mi
9722 Liberia Ave
Manassas, VA 20110
Bristow 20.71 mi
12705 Braemar Village Pz
Bristow, VA 20136
Burke 20.82 mi
9411 Old Burke Lake Rd
Burke, VA 22015
Bethesda 21.3 mi
4918 Fairmont Ave
Bethesda, MD 20814
Annandale 21.64 mi
7000 Columbia Pike
Annandale, VA 22003
Damascus 22.77 mi
9815 Main St
Damascus, MD 20872
Arlington, VA 23.29 mi
4801 1st St N
Arlington, VA 22203
Cathedral Heights 23.51 mi
3706 Macomb St NW
Washington, D.C., DC 20016
Olney 23.96 mi
18157 Village Center Dr
Olney, MD 20832
Downtown Silver Spring 24.94 mi
1133 East West Highway
Silver Spring, MD 20910
Lorton 25.06 mi
9027 Silverbrook Rd
Fairfax Station, VA 22039
West Washington 25.69 mi

Washington, DC 20009
Alexandria City 25.7 mi
4605 Duke Street
Alexandria, VA 22304
Lake Ridge 26.5 mi
12473 Dillingham Square
Lake Ridge, VA 22192
Frederick North 26.7 mi
905 W. 7th Street
Frederick, MD 21701
Northern Silver Spring 26.75 mi
732 Cloverly Street
Silver Spring, MD 20905
Alexandria 27.17 mi
6483 Old Beulah Street
Alexandria, VA 22315
Warrenton 27.42 mi
512 Fletcher Drive
Warrenton, VA 20186
Mount Airy 28.24 mi
411 E Ridgeville Blvd
Mt Airy, MD 21771
Capitol Hill DC 28.48 mi
621 Pennsylvania Ave SE
1st-floor unit
Washington, DC 20003
Dale City 28.99 mi
5512 Staples Mill Plaza
Dale City, VA 22193
Mount Vernon 29.66 mi
7696 H Richmond Hwy
Alexandria, VA 22306
Beltsville 30.89 mi
10914 Baltimore Ave
Beltsville, MD 20705
Clarksville 31.56 mi
12250 Clarksville Pike
Clarksville, MD 21029
Laurel 35.02 mi
10095 Washington Blvd N
Laurel, MD 20723
Woodmore 35.27 mi
9101 Woodmore Centre Drive
Lanham, MD 20706
Glenn Dale 35.83 mi
10559 Greenbelt Rd
Lanham, MD 20706
Sykesville 36.57 mi
1207 Liberty Rd.
Sykesville, MD 21784
Ellicott City 37.11 mi
3290 Pine Orchard Lane
Ellicott City, MD 21042
Winchester 37.62 mi
2512 S Pleasant Valley Rd
Winchester, VA 22601
Columbia 38.19 mi
8827 Centre Park Drive
Columbia, MD 21045
Stafford 39.58 mi
263 Garrisonville Road
Stafford, VA 22554
Bowie 41.26 mi
15231 Hall Rd
Bowie, MD 20721
Waldorf 42.24 mi
3022 Festival Way
Waldorf, MD 20601
Crofton 42.6 mi
1153 Route 3 North
Crofton, MD 21054
Owings Mills 44.15 mi
9433 Common Brook Rd #100
Owings Mills, MD 21117
Pikesville 46.84 mi
1433 Reisterstown Rd
Pikesville, MD 21208
Dunkirk 49.92 mi
10735 Town Center Blvd
Dunkirk, MD 20754