In 2017, after a decade of on-and-off work, Hales posted a preprint that offered a sort of blueprint for a proof. He proposed using a branch of mathematics called optimal control theory, which would be better suited, he believed, to exploring flip-flopping structures. To other mathematicians, an unapproachable problem had suddenly become feasible. “I was very impressed with the creativity,” Cohn said. “But on the other hand, I thought, it’ll take so much work to actually pull it off.”

Not long after Hales set out his blueprint, Vajjha arrived in Pittsburgh feeling a little lost, as many students do early on in graduate school. He was hoping to study formal methods — techniques used to verify software and hardware — and was attending all sorts of talks around town in search of the right problem to focus on. In one of them, he learned about the search for the best worst packer, and he found the deceptive trickiness of the problem intriguing. He was even more interested later that day when he found Hales’ preprint, which proposed a radically new approach to the problem.

The two met the following week. “I told him, ‘If this is so easy, why don’t you just do it?’” Vajjha recalled. Hales replied that they could probably tackle it together in about six months. Vajjha agreed. “Things are never that easy,” he recently said.

In order to prove that the rounded octagon was the shape with the worst packing, Hales and Vajjha effectively had to rule out every other possible shape. Even with constraints like central symmetry and convexity, they were staring down a problem with infinite potential answers, many of which exhibit strange behaviors that can make them appear to be viable solutions, when in fact they aren’t valid. There were candidate shapes, for example, that would flip-flop between straight lines and curves an infinite number of times, called “chattering” solutions. That might sound paradoxical, but such shapes might do better than a circle. Could they even be better than Reinhardt’s rounded octagon?

Hales’ voluminous proof of Kepler’s conjecture had used a computer-assisted approach that involved ruling out a nearly endless array of possible packings with brute force. It was considered pioneering — and, at the time, a bit controversial, as reviewers found the programs hard to verify. Hales hoped to use similar methods to find the worst shape, but potential chattering solutions presented a roadblock. “If things are switching around infinitely many times, then it’s not going to be easy to do on a computer,” Hales said.

Doing away with those and other obscure structures required finding creative ways to rule them out. They tried simplifying the problem by introducing new symmetric constraints and then working their way back up to the original problem. “Just as in physics, there’s this idea in mathematics where if you have symmetry you also have conservation laws,” Hales said. Those laws could help rule some of the structures out.