In a sense, the computer and the Collatz conjecture are a perfect match. For one, as Jeremy Avigad, a logician and professor of philosophy at Carnegie Mellon notes, the notion of an iterative algorithm is at the foundation of computer science—and Collatz sequences are an example of an iterative algorithm, proceeding step-by-step according to a deterministic rule. Similarly, showing that a process terminates is a common problem in computer science. “Computer scientists generally want to know that their algorithms terminate, which is to say, that they always return an answer,” Avigad says. Heule and his collaborators are leveraging that technology in tackling the Collatz conjecture, which is really just a termination problem.
“The beauty of this automated method is that you can turn on the computer, and wait.”
Jeffrey Lagarias
Heule’s expertise is with a computational tool called a “SAT solver”—or a “satisfiability” solver, a computer program that determines whether there is a solution for a formula or problem given a set of constraints. Though crucially, in the case of a mathematical challenge, a SAT solver first needs the problem translated, or represented, in terms that the computer understands. And as Yolcu, a PhD student with Heule, puts it: “Representation matters, a lot.”
A longshot, but worth a try
When Heule first mentioned tackling Collatz with a SAT solver, Aaronson thought, “There is no way in hell this is going to work.” But he was easily convinced it was worth a try, since Heule saw subtle ways to transform this old problem that might make it pliable. He’d noticed that a community of computer scientists were using SAT solvers to successfully find termination proofs for an abstract representation of computation called a “rewrite system.” It was a longshot, but he suggested to Aaronson that transforming the Collatz conjecture into a rewrite system might make it possible to get a termination proof for Collatz (Aaronson had previously helped transform the Riemann hypothesis into a computational system, encoding it in a small Turing machine). That evening, Aaronson designed the system. “It was like a homework assignment, a fun exercise,” he says.
“In a very literal sense I was battling a Terminator—at least a termination theorem prover.”
Scott Aaronson
Aaronson’s system captured the Collatz problem with 11 rules. If the researchers could get a termination proof for this analogous system, applying those 11 rules in any order, that would prove the Collatz conjecture true.
Heule tried with state-of-the-art tools for proving the termination of rewrite systems, which didn’t work—it was disappointing if not so surprising. “These tools are optimized for problems that can be solved in a minute, while any approach to solve Collatz likely requires days if not years of computation,” says Heule. This provided motivation to hone their approach and implement their own tools to transform the rewrite problem into a SAT problem.
MARIJN HEULE
Aaronson figured it would be much easier to solve the system minus one of the 11 rules—leaving a “Collatz-like” system, a litmus test for the larger goal. He issued a human-versus-computer challenge: The first to solve all subsystems with 10 rules wins. Aaronson tried by hand. Heule tried by SAT solver: He encoded the system as a satisfiability problem—with yet another clever layer of representation, translating the system into the computer’s lingo of variables that can be either 0s and 1s—and then let his SAT solver run on the cores, searching for evidence of termination.
MARIJN HEULE
They both succeeded in proving that the system terminates with the various sets of 10 rules. Sometimes it was a trivial undertaking, for both the human and the program. Heule’s automated approach took at most 24 hours. Aaronson’s approach required significant intellectual effort, taking a few hours or even a day—one set of 10 rules he never managed to prove, though he firmly believes he could have, with more effort. “In a very literal sense I was battling a Terminator,” Aaronson says—“at least a termination theorem prover.”
Yolcu has since fine-tuned the SAT solver, calibrating the tool to better fit the nature of the Collatz problem. These tricks made all the difference—speeding up the termination proofs for the 10-rule subsystems and reducing runtimes to mere seconds.
“The main question that remains,” says Aaronson, “is, What about the full set of 11? You try running the system on the full set and it just runs forever, which maybe shouldn’t shock us, because that is the Collatz problem.”
As Heule sees it, most research in automated reasoning has a blind eye for problems that require lots of computation. But based on his previous breakthroughs he believes these problems can be solved. Others have transformed Collatz as a rewrite system, but it’s the strategy of wielding a fine-tuned SAT solver at scale with formidable compute power that might gain traction toward a proof.
So far, Heule has run the Collatz investigation using about 5,000 cores (the processing units powering computers; consumer computers have four or eight cores). As an Amazon Scholar, he has an open invitation from Amazon Web Services to access “practically unlimited” resources—as many as one million cores. But he’s reluctant to use significantly more.
“I want some indication that this is a realistic attempt,” he says. Otherwise, Heule feels he’d be wasting resources and trust. “I don’t need 100% confidence, but I really would like to have some evidence that there’s a reasonable chance that it’s going to succeed.”
Supercharging a transformation
“The beauty of this automated method is that you can turn on the computer, and wait,” says the mathematician Jeffrey Lagarias, of the University of Michigan. He’s toyed with Collatz for about fifty years and become keeper of the knowledge, compiling annotated bibliographies and editing a book on the subject, “The Ultimate Challenge.” For Lagarias, the automated approach brought to mind a 2013 paper by the Princeton mathematician John Horton Conway, who mused that the Collatz problem might be among an elusive class of problems that are true and “undecidable”—but at once not provably undecidable. As Conway noted: “… it might even be that the assertion that they are not provable is not itself provable, and so on.”
“If Conway is right,” Lagarias says, “there will be no proof, automated or not, and we will never know the answer.”
