The computer scientist Marijn Heule is always on the lookout for a good mathematical challenge. An associate professor at Carnegie Mellon University, Heule has an impressive reputation for solving intractable math problems with computational tools. His 2016 result with the “Boolean Pythagorean triples problem” was an enormous headline-grabbing proof: “Two hundred terabyte maths proof is largest ever.” Now he’s deploying an automated approach to attack the beguilingly simple Collatz conjecture.

First proposed (according to some accounts) in the 1930s by the German mathematician Lothar Collatz, this number theory problem provides a recipe, or algorithm, for generating a numerical sequence: Start with any positive integer. If the number is even, divide by two. If the number is odd, multiply by three and add one. And then do the same, again and again. The conjecture asserts that the sequence will always end up at 1 (and then continually cycle through 4, 2, 1).

The number 5, for instance, generates only six terms:

5, 16, 8, 4, 2, 1

The number 27 cycles through 111 terms, oscillating up and down—at its height reaching 9,232—before eventually landing at 1.

The number 40 generates another brief sequence:

40, 20, 10, 5, 16, 8, 4, 2, 1

To date, the conjecture has been checked by computer for all starting values up to nearly 300 billion billion and every number eventually reaches 1.

Most researchers believe the conjecture is true. It has enticed multitudes of mathematicians and non-mathematicians alike, but nobody has produced a proof. In the early 1980s, the Hungarian mathematician Paul Erdős declared: “Mathematics is not yet ready for such problems.”

“What we want to know is whether humans or computers are better at solving such problems.”

Marijn Heule

“And he’s probably right,” says Heule. For Heule, Collatz’s allure isn’t so much the prospect of a breakthrough as it is advancing automated reasoning techniques. After tinkering with it for five years, Heule and his collaborators, Scott Aaronson and Emre Yolcu, recently posted a paper on the arXiv preprint server. “Although we do not succeed in proving the Collatz conjecture,” they write, “we believe that the ideas here represent an interesting new approach.”

“It’s a noble failure,” says Aaronson, a computer scientist at the University of Texas at Austin. A failure because they didn’t prove the conjecture. Noble because they made progress in another sense: Heule views it as a starting point in determining whether humans or computers are better at proving such problems.

### Translating math to computation

For many math problems, computers are hopeless, since they don’t have access to the vast oeuvre of mathematics amassed through history. But sometimes computers excel where humans are hopeless. Tell a computer what a solution looks like—give it a target and a well-defined search space—and then with brute force the computer might find it. Though it’s a matter of debate whether computational results amount to meaningful additions to the mathematical canon. The traditional view is that only human creativity and intuition, via concepts and ideas, extend the reach of mathematics, whereas advancements via computing are often dismissed as engineering.

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.”

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

————

By: Siobhan Roberts
Title: Are computers ready to solve this notoriously unwieldy math problem?