In a sense, the computer and Collatz’s assumptions match perfectly. First, as noted by Jeremy Avigad, a logician and professor of philosophy at Carnegie Mellon, the notion of an iterative algorithm is the foundation of computer science – and Collatz’s sequences are an example of an iterative algorithm, going step by step to a deterministic rule. Similarly, showing that the process is complete is a common problem in computing. “Computer scientists generally want to know that their algorithms are interrupted, which means they always give an answer,” says Avigad. Heule and his collaborators use this technology in solving Collatz’s assumption, which is really just a problem of discontinuity.
“The beauty of this automated method is that you can turn on your computer and wait.”
Heule’s expertise is in a computer tool called a “SAT solver” – or “satisfaction” solver, a computer program that determines whether there is a solution to a formula or a problem given a set of constraints. Although crucial, in the case of a mathematical challenge, the SAT solver first needs a problem translated or presented in terms that the computer understands. And as Yolcu, a doctoral student at Heule, says: “Representation is important, a lot.”
Longshot, but worth a try
When Heule first mentioned solving Collatz with a SAT solver, Aaronson thought, “There’s no way this is going to work.” But he was easily convinced that it was worth a try, because Heule saw subtle ways to transform this old problem that could make him flexible. He noted that the computer science community is using SAT solvers to successfully find evidence of the completion of an abstract computational representation called a “transcription system.” It was a long time, but he suggested to Aaronson that converting Collatz’s assumption into a transcription system could make it possible to obtain proof of the breakdown for Collatz (Aaronson had previously helped transform Riemann’s hypothesis into a computational system, encoding it in a small Turing machine). That evening Aaronson designed the system. “It was like homework, a fun exercise,” he says.
Aaronson’s system caught Collatz’s problem with 11 rules. If researchers could obtain termination evidence for this analog system, applying these 11 rules in any order, it would prove Collatz’s assumption true.
Heule tried the most modern tools for proving the interruption of the transcription system, which failed – it was disappointing, if not surprising. “These tools are optimized for problems that can be solved in a minute, while any approach to solving Collatz probably requires days, if not years of computation,” Heule says. This gave them the motivation to perfect their approach and apply their own tools to transform the rewriting problem into a SAT problem.
Aaronson concluded that it would be much easier to solve the system minus one of the 11 rules – leaving the system “similar to Collatz”, a litmus test for a larger goal. He announced the man-versus-computer challenge: the first to solve all 10-rule subsystems. Aaronson tried it manually. Heule tried the SAT solver: He coded the system as a satisfying problem – with another smart layer of representation, translating the system into computer lingo variables that could be 0 and 1 – and then let his SAT solver run on cores, looking for evidence of termination.
They both managed to prove that the system terminates using different sets of 10 rules. Sometimes it was a trivial undertaking, both for the people and for the program. Heule’s automated access lasted a maximum of 24 hours. Aaronson’s approach required significant intellectual effort, lasting several hours or even a day – one set of 10 rules he never managed to prove, though he firmly believes he could, with more effort. “In a very literal sense, I fought the Terminator,” says Aaronson – “at least by proof of the termination theorem.”
Yolca has since been fine-tuned with the SAT solver, calibrating the tool to better fit the nature of the Collatz problem. These tricks made all the difference – speeding up the proof of completion for 10-rule subsystems and reducing execution time to just a few seconds.
The main question that remains, “says Aaronson,” is, what about the set of 11? You’re trying to run the system on a complete set and it just works forever, which might not shock us, because that’s Collatz’s problem. “
As Heule sees, most research in automated reasoning has a blind eye to problems that require a lot of computation. But based on his previous discoveries, he believes these problems can be solved. Others are transformed Collatz have a overwrite the system, but it is a strategy of managing a finely tuned SAT solver on a scale with frightening computing power that could gain strength according to evidence.
So far, Heule has led the Collatz investigation using about 5,000 cores (processor units that power computers; consumer computers have four or eight cores). Like Amazon Scholar, he has an open call from Amazon Web Services to access “virtually unlimited” resources – as many as a million cores. But he is reluctant to use much more.
“I want indications that this is a realistic attempt,” he says. Otherwise, Heule feels he would be wasting resources and trust. “I don’t need 100% confidence, but I’d really like to have some evidence that there’s a reasonable chance it’ll work.”
Complementing the transformation
“The beauty of this automated method is that you can turn on the computer and wait,” says mathematician Jeffrey Lagarias of the University of Michigan. He played with Collatz for about fifty years and became a custodian of knowledge, compiling annotated bibliographies and editing a book on the subject, “The ultimate challenge.”For Lagarias, the automated approach was reminiscent of a 2013 Princeton mathematician John Horton Conway, who thought that Collatz’s problem might be among an unattainable class of problems that are true and “indecisive,” but suddenly not provably indecisive. As Conway remarked, “… it could even be that the claim that they are not provable is not in itself proven, and so on.”
“If Conway is right,” Lagarias says, “there will be no evidence, automated or not, and we will never know the answer.”