In a sense, the computer and the Collatz conjecture are perfectly compatible. On the one hand, as Jeremy Avigad, logician and professor of philosophy at Carnegie Mellon, notes, the notion of iterative algorithm is the basis of computer science – and Collatz sequences are an example of an iterative algorithm, proceeding step step by step according to a deterministic rule. Likewise, showing that a process has ended is a common problem in computer science. “IT people generally want to know that their algorithms are terminating, that is, they always return a response,” says Avigad. Heule and colleagues take advantage of this technology to tackle 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.”
Heule’s expertise lies in a computational tool called a “SAT solver” or “satisfiability solver”, a computer program that determines whether there is a solution for a formula or a problem given a set of constraints. Although in essence, in the case of a mathematical challenge, an SAT solver first needs the problem to be translated, or represented, in terms that the computer understands. And as Yolcu, doctoral student at Heule, says: “Representation matters a lot.
A long shot, but worth a try
When Heule first mentioned tackling Collatz with a SAT solver, Aaronson thought, “There’s no way this will work.” But he was easily convinced it was worth a try, as Heule saw subtle ways to turn this old problem that might make him malleable. He had noticed that a community of computer scientists were using SAT solvers to successfully find termination proofs for an abstract representation of calculus called a “rewrite system”. It was a long time, but he suggested to Aaronson that turning the Collatz conjecture into a rewrite system could yield a proof of termination for Collatz (Aaronson had previously helped turn the Riemann hypothesis into a computational system. , by encoding it in a small Turing machine). That night Aaronson designed the system. “It was like an assignment, a fun exercise,” he says.
Aaronson’s system captured the Collatz problem with 11 rules. If the researchers could obtain a proof of termination for this analogous system, by applying these 11 rules in any order, it would prove that the Collatz conjecture is true.
Heule tried with cutting edge tools to prove stopping rewrite systems, which didn’t work – it was disappointing, if not surprising. “These tools are optimized for problems that can be solved in a minute, whereas any approach to solving Collatz probably requires days or even years of computation,” Heule explains. This motivated them to refine their approach and implement their own tools to turn the rewrite problem into a SAT problem.
Aaronson thought it would be much easier to solve the system minus one of the 11 rules – leaving a “Collatz-type” system, a litmus test for the larger goal. He launched a human versus computer challenge: the first to solve all subsystems with 10 rules wins. Aaronson tried by hand. Heule tried by the SAT solver: he encoded the system as a satisfiability problem – with yet another layer of intelligent representation, translating the system into the parlance of computer variables which can be 0’s and 1’s, then let his SAT solver run on cores, looking for proof of termination.
They both managed to prove that the system ends with the different sets of 10 rules. Sometimes it was a trivial undertaking, both for the human and for the program. Heule’s automated approach took at most 24 hours. Aaronson’s approach required a great deal of intellectual effort, taking a few hours or even a day – a set of 10 rules that he has never been able to prove, although he firmly believes he could have done so. with more effort. “In a very literal sense, I was fighting a Terminator,” Aaronson says – “at least one termination theorem prover.”
Yolcu has since refined the SAT solver, calibrating the tool to better suit the nature of the Collatz problem. These tips made all the difference, speeding up proofs of termination for 10 rule subsystems and reducing execution times to just seconds.
“The main question that remains,” says Aaronson, “is, what about the full set of 11? You’re trying to run the system on the full set and it works forever, which maybe shouldn’t shock us because that’s Collatz’s problem.
According to Heule, most research on automated reasoning turns a blind eye to problems that require a lot of calculation. But based on his previous breakthroughs, he believes these issues can be resolved. Others have Collatz transformed have a rewrite system, but it is the strategy of using a large-scale refined SAT solver with formidable computing power that could gain ground towards a proof.
So far, Heule has conducted the Collatz investigation using around 5,000 cores (the processing units powering computers; consumer computers have four or eight cores). As an Amazon Scholar, he received an open invitation from Amazon Web Services to access “virtually unlimited” resources, up to one million cores. But he hesitates to use much more.
“I want an indication that this is a realistic attempt,” he said. Otherwise, Heule thinks he would waste resources and trust. “I don’t need 100% trust, but I would really like to have proof that there is a reasonable chance that it will be successful.”
Supercharging a 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 some fifty years and became the keeper of knowledge, compiling annotated bibliographies and editing a book on the subject, “The ultimate challenge.”For Lagarias, the automated approach made one think of a 2013 paper by Princeton mathematician John Horton Conway, who thought the Collatz problem might be part of an elusive class of problems that are true and “undecidable” – but at the same time not provable undecidable. As Conway noted: “… it may even be that the claim that they are not provable is not itself provable, and so on.
“If Conway is right,” says Lagarias, “there will be no proof, automated or not, and we will never know the answer.”