The 200-terabyte proof

Here’s a puzzle you can do on a napkin. Color the numbers 1 to 5 red or blue so that there’s no x, y and z of the same color with x + y = z. (x and y can be the same number, so 1 + 1 = 2 counts.)

Say 1 is red. Then 2 has to be blue, because 1 + 1 = 2. Then 4 has to be red, because 2 + 2 = 4. Now 3: if it’s red, 1 + 3 = 4 is all red, so 3 is blue. And now 5 is stuck, since 1 + 4 = 5 rules out red and 2 + 3 = 5 rules out blue. If 1 had started blue, swap the colors and the same thing happens. So you can do 1 to 4 (red 1 and 4, blue 2 and 3), and you can’t do 1 to 5.

That’s Schur’s theorem, from 1916, for two colors: however you color the integers with a fixed number of colors, eventually you’re forced to make a monochromatic x + y = z. The largest n you can get away with is called the Schur number. For two colors it’s 4, for three it’s 13, for four it’s 44, and that last one was settled by computer search in 1965. It’s one of the starting points of Ramsey theory, the part of combinatorics whose slogan is roughly “complete disorder is impossible”: color anything big enough and you’re forced to make some pattern.

I’ve had a soft spot for this stuff for a long time, mostly because the questions are so easy to state and the answers so hard to get. Which brings me to the paper that went up on arXiv on May 3rd, Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer, by Marijn Heule, Oliver Kullmann and Victor Marek.

The question

Same idea, different equation. Can you color the positive integers red and blue so that no Pythagorean triple, a² + b² = c², is all one color? Ron Graham offered $100 for the answer, the paper says, over two decades ago. The best anybody had done was a valid coloring of 1 to 7,664, by Cooper and Overstreet. Nobody knew whether that could go on forever.

The answer is no. The numbers 1 to 7,824 can be colored this way. The numbers 1 to 7,825 can’t. And the proof that you can’t is a SAT solver’s output, which in the format they checked it in is almost 200 terabytes.

It’s worth playing with small cases first, because you can see why it’s easy at the start. Up to 30 there are only 11 triples, and lots of numbers aren’t in any triple at all, so they don’t matter and you can color them however you like. Here’s a valid coloring I found with a ten-line backtracking script:

Look at the blue numbers: 5, 10, 15, 20, and then 24. That’s not a coincidence, and it’s my favorite bit of the whole thing. Every Pythagorean triple has a number divisible by 5 in it. (Squares mod 5 can only be 0, 1 or 4. If neither a nor b is a multiple of 5, a² + b² mod 5 is 1 + 1 = 2, 4 + 4 = 3, or 1 + 4 = 0, and 2 and 3 aren’t squares mod 5, so c² ≡ 0 and c is a multiple of 5.) So “multiples of 5 are blue, everything else is red” means the red side can never contain a whole triple. The blue side breaks when all three numbers are multiples of 5, which happens when the triple is 5 times another triple, like 15-20-25. So you flip 25 to red. But then 7-24-25 is all red, so you flip 24 to blue. And so on, each patch causing new problems somewhere else. Up to 30 it settles quickly. Up to 7,825 there are 9,472 triples using 6,494 different numbers, all tangled together, and the patches never settle.

Turning it into SAT

A SAT solver takes a formula in boolean variables, written as a list of clauses (ORs of variables or their negations), and either finds an assignment that makes every clause true or reports that there isn’t one. The encoding here is about as simple as encodings get: one variable per number, true means red. Each triple (a, b, c) becomes two clauses, “at least one of a, b, c is red” and “at least one of them isn’t”. In the DIMACS format every solver reads, a clause is a line of variable numbers, negative for NOT, ending with 0:

import math, sys

n = int(sys.argv[1])
clauses = []
for c in range(1, n + 1):
    for a in range(1, c):
        b = int(math.sqrt(c * c - a * a))
        if a < b and a * a + b * b == c * c:
            clauses.append("%d %d %d 0" % (a, b, c))      # not all blue
            clauses.append("-%d -%d -%d 0" % (a, b, c))   # not all red

print("p cnf %d %d" % (n, len(clauses)))
print("\n".join(clauses))

Run that with 7825 and you get a header of p cnf 7825 18944, which matches the clause count in the paper. It’s a 340 KB text file. You could email it. That’s what’s so strange about this problem: the input is tiny, and the question “is there an assignment?” is easy to state about it, and the answer took about four CPU-years.

For n = 7,824 the solver finds a coloring, and checking it takes a second, you just look at every triple. For 7,825 the answer is “unsatisfiable”, and that’s the hard one, because “my program searched and didn’t find anything” is not a proof. Programs have bugs. SAT solvers are very heavily optimized C, and they have bugs too.

Cube and conquer

The way they actually solved it is a technique Heule has been developing for a few years, cube-and-conquer, and the paper’s subtitle is basically the recipe.

First they simplify. Any number that appears in only one triple can always be colored to satisfy that triple, so you can drop the triple, and that can make other numbers appear in only one triple, and so on. (They also fix one variable’s color, 2520’s, since swapping all the colors of a solution gives another solution.) After that, the 7,825 problem is down to 3,745 variables and 14,672 clauses.

Then they split. A “look-ahead” solver, which is slow per decision but very good at choosing which variable to branch on, chops the problem into a million subproblems. Each subproblem is a “cube”, a set of decisions like “2520 is red, 3000 is blue, 1105 is red, …”, between 12 and 49 decisions long. Then a regular CDCL solver, the fast, clause-learning kind, takes each cube and proves it can’t be extended to a full coloring.

They picked a million because their cluster allocation was 800 cores and a million divides evenly, and because it made most subproblems take under two minutes. (I love that a number in a landmark result was chosen for scheduling convenience.) It ran on the Stampede supercomputer at the Texas Advanced Computing Center, and with 800 cores going it took about two days. The total was about 35,000 CPU-hours. Their first try with default heuristics was heading for something like 300,000 CPU-hours, and they got it down by almost an order of magnitude by hand-tuning the look-ahead heuristics, which is the part of the paper with the most actual new research in it and the part I understand least.

The proof nobody will read

What makes this a proof rather than a claim is logging. Modern SAT solvers can log their reasoning as they go, in a format called DRAT. Every clause the solver learns gets written down, and every one of them is something a much simpler checker program can verify follows from what came before, using unit propagation (the dumbest possible inference step: if all but one literal in a clause is false, the last one has to be true). Mostly. The “RAT” part also allows a few kinds of clause addition that don’t strictly follow but provably don’t change whether the formula is satisfiable, which is what lets you write down things like the symmetry-breaking step.

So you don’t have to trust the solver, tens of thousands of lines of clever C. You have to trust the checker, which is small and simple enough to read in an afternoon. The checker reads through the proof, confirms every step, and confirms that you end up at the empty clause, a contradiction. Plus one more check, that the million cubes between them cover every case.

The proof of all million cubes, in DRAT, is almost 200 terabytes. Compressed with everything they could throw at it, it was still 14 terabytes, which is too big to just put on a website. So they released something cleverer: the cube files, which compress down to 68 gigabytes, and from which anyone with enough CPU time can regenerate the full proof and check it. Regenerating takes about 13,000 CPU-hours and checking takes about 16,000.

There’s a neat little glimpse into why the answer is no, in section 6. In every solution of their simplified 7,824 formula, 5180 and 5865 come out the same color, and 625 and 7800 come out the other color. And 5180² + 5865² = 7825², and 625² + 7800² = 7825². I checked both, because of course I did. So 7,825 can’t be red and can’t be blue. That doesn’t explain why those four numbers are forced, it just shows you where the trap closes.

How I feel about it

This has happened before, sort of. The four color theorem in 1976 needed a computer to check about two thousand configurations, and plenty of mathematicians were unhappy about it for years. Tom Hales’ proof of the Kepler conjecture was finished as a formal, machine-checked proof only in 2014. And two years ago Konev and Lisitsa used a SAT solver to settle a special case of the Erdős discrepancy problem, with a proof of about 13 gigabytes, which seemed big at the time. Then last September Terry Tao proved the whole Erdős discrepancy conjecture, by hand, on a few dozen pages, and nobody’s used the 13 GB proof for anything since.

That’s my main hesitation. A proof, the way I was taught it, is supposed to make you understand why something is true. This one tells you, with as much certainty as anything in math, that it’s true, and essentially nothing about why. Nobody’s going to read 200 terabytes. You can’t learn a technique from it or generalize it. The paper’s own conjecture, that the same thing happens for any number of colors, is completely untouched.

On the other hand, I’m a programmer, and I find it hard not to be impressed. The question sat open for decades, it’s now settled, the settlement is checkable by anyone with the patience and a few thousand dollars of compute, and the tools that did it (cube-and-conquer, DRAT proofs) are general. I suspect there are quite a few combinatorics problems where “how many?” questions are now within reach of exactly this approach, and that we’ll see more of these. I’d still trade all 200 terabytes for a two-page argument about why 7,825 is special, if anyone ever finds one.