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.

Original story reprinted with permission from *Quanta Magazine*, an editorially independent publication of the Simons Foundation whose mission is to enhance public understanding of science by covering research developments and trends in mathematics and the physical and life sciences.

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.

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).