As an undergraduate at the University of Chile, Bernardo Subercaseaux took a dim view of using computers to do math. It seemed antithetical to real intellectual discovery.

“There’s some instinct or gut reaction against using computers to solve your problems, like it goes against the ideal beauty or elegance of a fantastic argument,” he said.

But then in 2020 Subercaseaux fell in love, and as often happens, his priorities changed. The object of his obsession was a question he saw on an online forum. Most problems he scanned and forgot, but this one caught his eye. He swiped right.

“The first thing I did was to like the post in the Facebook group, hoping to get a notification later when somebody else posted a solution,” he said.

The question was about filling an infinite grid with numbers. It was not, as it turned out, the kind of problem one solves on a lark. In order to do it, Subercaseaux had to leave Chile for graduate school at Carnegie Mellon University.

There, in August 2021, he had a fortuitous encounter with Marijn Heule, a computer scientist who uses massive computing power to solve hard math questions. Subercaseaux asked Heule if he wanted to attempt the problem, kicking off a collaboration that culminated this January in a proof that can be summed up with a single number: 15.

Every Possible Way

In 2002, Wayne Goddard of Clemson University and some like-minded mathematicians were spitballing problems in combinatorics, trying to come up with new twists on the field’s mainstay questions about coloring maps given certain constraints.

Eventually they landed on a problem that starts with a grid, like a sheet of graph paper that goes on forever. The goal is to fill it with numbers. There’s just one constraint: The distance between each occurrence of the same number must be greater than the number itself. (Distance is measured by adding together the vertical and horizontal separation, a metric known as “taxicab” distance for the way it resembles moving on gridded urban streets.) A pair of 1s cannot occupy adjoining cells, which have a taxicab distance of 1, but they can be placed in directly diagonal cells, which have a distance of 2.

Initially, Goddard and his collaborators wanted to know whether it was even possible to fill an infinite grid with a finite set of numbers. But by the time he and his four collaborators published this “packing coloring” problem in the journal Ars Combinatoria in 2008, they had proved that it can be solved using 22 numbers. They also knew that there was no way it could be solved with only five numbers. That meant the actual answer to the problem — the minimum number of numbers needed — lay somewhere in between.

The researchers didn’t actually fill an infinite grid. They didn’t have to. Instead, it’s enough to take a small subset of the grid — say a 10-by-10 square — fill that with numbers, then show that copies of the filled subset can be placed next to each other, the way you’d cover a floor with copies of a tile.

When Subercaseaux first learned of the problem, he started looking for tiles using pen and paper. He would sketch grids of numbers, cross them out, try again. He soon tired of that approach, and he asked a friend to design a web-based tool that resembled the game Minesweeper and allowed him to test combinations faster. After a few more weeks of work he’d convinced himself there was no way to pack a grid with eight numbers, but he couldn’t get any further than that — there were just too many potential shapes the tiles could take, and too many different ways they could be filled with numbers.

The problem, as would later become clear, is that it’s vastly more difficult to show that the grid can’t be covered by a certain set of numbers than to show that it can. “It isn’t just showing that one way doesn’t work, it’s showing that every possible way doesn’t work,” Goddard said.

After Subercaseaux started at CMU and convinced Heule to work with him, they quickly found a way to cover the grid with 15 numbers. They were also able to rule out the possibility of solving the problem with only 12 numbers. But their feelings of triumph were short-lived, as they realized that they’d merely reproduced results that had been around for a long time: As far back as 2017, researchers had known the answer wasn’t less than 13 or greater than 15.

For a first-year grad student who’d roped a big-time professor into working on his pet problem, it was an unsettling discovery. “I was horrified. I had basically been working for several months on a problem without realizing this, and even worse, I had made Marijn waste his time on it!” Subercaseaux wrote in a blog post recapping their work.

Heule, however, found the discovery of past results invigorating. It demonstrated that other researchers found the problem important enough to work on, and confirmed for him that the only result worth obtaining was to solve the problem completely.

“Once we figured out there had been 20 years of work on the problem, that completely changed the picture,” he said.

Avoiding the Vulgar

Over the years, Heule had made a career out of finding efficient ways to search among vast possible combinations. His approach is called SAT solving — short for “satisfiability.” It involves constructing a long formula, called a Boolean formula, that can have two possible results: 0 or 1. If the result is 1, the formula is true, and the problem is satisfied.

For the packing coloring problem, each variable in the formula might represent whether a given cell is occupied by a given number. A computer looks for ways of assigning variables in order to satisfy the formula. If the computer can do it, you know it’s possible to pack the grid under the conditions you’ve set.

Unfortunately, a straightforward encoding of the packing coloring problem as a Boolean formula could stretch to many millions of terms — a computer, or even a fleet of computers, could run forever testing all the different ways of assigning variables within it.

“Trying to do this brute force would take until the universe finishes if you did it naïvely,” Goddard said. “So you need some cool simplifications to bring it down to something that’s even possible.”

Moreover, every time you add a number to the packing coloring problem, it becomes about 100 times harder, due to the way the possible combinations multiply. This means that if a bank of computers working in parallel could rule out 12 in a single day of computation, they’d need 100 days of computation time to rule out 13.

Heule and Subercaseaux regarded scaling up a brute-force computational approach as vulgar, in a way. “We had several promising ideas, so we took the mindset of ‘Let’s try to optimize our approach until we can solve this problem in less than 48 hours of computation on the cluster,’” Subercaseaux said.

To do that, they had to come up with ways of limiting the number of combinations the computing cluster had to try.

“[They] want not just to solve it, but to solve it in an impressive way,” said Alexander Soifer of the University of Colorado, Colorado Springs.

Heule and Subercaseaux recognized that many combinations are essentially the same. If you’re trying to fill a diamond-shaped tile with eight different numbers, it doesn’t matter if the first number you place is one up and one to the right of the center square, or one down and one to the left of the center square. The two placements are symmetric with each other and constrain your next move in exactly the same way, so there’s no reason to check them both.

Heule and Subercaseaux added rules that allowed the computer to treat symmetric combinations as equivalent, reducing the total search time by a factor of eight. They also employed a technique Heule had developed in previous work called cube and conquer, which allowed them to test more combinations in parallel with each other. If you know a given cell has to contain either 3, 5 or 7, you can split the problem and test each of the three possibilities simultaneously on different sets of computers.

By January 2022 these improvements allowed Heule and Subercaseaux to rule out 13 as the answer to the packing coloring problem in an experiment that required less than two days of computing time. This left them with two possible answers: 14 or 15.

A Big Plus

To rule out 14 — and solve the problem — Heule and Subercaseaux had to find additional ways to speed the computer search.

Initially, they had written a Boolean formula that assigned variables to each individual cell in the grid. But in September 2022, they realized that they did not need to proceed on a cell-by-cell basis. Instead, they discovered that it was more effective to consider small regions comprised of five cells in the shape of a plus sign.

They rewrote their Boolean formula so that several variables represented questions such as: Is there a 7 somewhere within this plus-shaped region? The computer did not need to identify exactly where in the region the 7 might be. It just needed to determine whether it was in there or not — a question which requires significantly fewer computational resources to answer.

“Having variables that talk about only pluses instead of specific locations turned out to be way better than talking about them in specific cells,” Heule said.

Aided by the efficiency of the plus search, Heule and Subercaseaux ruled out 14 in a computer experiment in November 2022 that ended up taking less time to run than the one they’d used to rule out 13. They spent the next four months verifying that the computer’s conclusion was correct — almost as much time as they’d spent enabling the computer to arrive at that conclusion in the first place.

“It was gratifying to think that what we’d spawned as a sort of side question in some random journal had caused groups of people to spend, as it turned out, months of their time trying to work out how to solve it,” Goddard said.

For Subercaseaux, it was the first real triumph of his research career. And while it may not have been the type of discovery he’d idealized when he first contemplated working in mathematics, he found that in the end, it had its own intellectual rewards.

“It’s not understanding of the form where you give me a blackboard and I can show you why it’s 15,” he said. “But we have gained understanding of how the constraints of the problem operate, how much better it is to have a 6 here or a 7 there. We have gained a lot of intuitive understanding.”