Carnegie Mellon University scientists solve 90-year-old math puzzle

Think solving a math problem isn’t exciting?

Try telling that to John Mackey, part of a team of Carnegie Mellon University computer scientists and mathematicians that spent four months solving the last piece of Keller’s conjecture, a geometry problem that’s been out there for over nine decades.

“I was really happy when we solved it, but then I was a little sad that the problem was gone. But then I felt happy again. There’s just this feeling of satisfaction,” said Mackey, a teaching professor in CMU’s Computer Science Department and Department of Mathematical Sciences for whom Keller’s conjecture has been the Holy Grail of math problems.

Mackey has been trying to solve Keller’s conjecture for 30 years, dating back to his days as a graduate student. It’s named for German mathematician Ott-Heinrich Keller, who formed the problem.

“The problem has intrigued many people for decades, almost a century,” said Marijn Heule, a CMU associate professor of computer science who came up with the approach to solving the problem. “This is really a showcase for what can be done now that was not possible previously.”

As CMU spokesman Byron Spice explained it, “Heule has used an SAT solver — a computer program that uses propositional logic to solve satisfiability (SAT) problems — to conquer several math challenges, including the Pythagorean triple problem and Schur number 5.

“An SAT solver requires structuring the problem using a propositional formula — (A or not B) and (B or C), etc. — so the solver can examine all of the possible variables for combinations that will satisfy all of the conditions,” Spice said.

The researchers’ published work, “The Resolution of Keller’s Conjecture,” opens with an explanation for the general public: “The conjecture involves a statement regarding tiling: Consider tiling a floor with square tiles, all of the same size. Is it the case that any gap-free tiling results in at least two fully connected tiles, i.e., tiles that have an entire edge in common?” The problem considers the pattern in a three-dimensional space. In 1930, Professor Keller “conjectured that it holds for any number of dimensions.” And then fellow mathematicians were off to the races.

In the end, it came down to four months of computer programming and a half hour of computation using a cluster of computers.

“There are many ways to make these translations, and the quality of the translation typically makes or breaks your ability to solve the problem,” Heule said. “The reason we succeeded is that John has decades of experience and insight into this problem, and we were able to transform it into a computer-generated search.”

While it all might be a bit much for the non-mathematical to comprehend, the drama of finding the solution is akin to the plot of the Pulitzer Prize-winning play “Proof,” in which the discovery of a groundbreaking proof about prime numbers drives the story.

“We can have real confidence in the correctness of this result,” Heule said.

A paper describing the resolution by Heule, Mackey, Joshua Brakensiek, a double major in mathematical sciences and computer science, and David Narvaez, a Ph.D. student at the Rochester Institute of Technology who was a visiting researcher in 2019, won a Best Paper award at the International Joint Conference on Automated Reasoning in June.