Computer generated math proof is largest ever at 200 terabytes

(Phys.org)—A trio of researchers has solved a single math problem by using a supercomputer to grind through over a trillion color combination possibilities, and in the process has generated the largest math proof ever—the text of it is 200 terabytes in size. In their paper uploaded to the preprint server arXiv, Marijn Heule with the University of Texas, Oliver Kullmann with Swansea University and Victor Marek with the University of Kentucky outline the math problem, the means by which a supercomputer was programmed to solve it, and the answer which the proof was asked to provide.

The has been named the boolean Pythagorean Triples problem and was first proposed back in the 1980's by mathematician Ronald Graham. In looking at the Pythagorean formula: a2 + b2 = c2, he asked, was it possible to label each a non-negative integer, either blue or red, such that no set of integers a, b and c were all the same color. He offered a reward of \$100 to anyone who could solve the problem.

To solve this problem the researchers applied the Cube-and-Conquer paradigm, which is a hybrid of the SAT method for hard problems. It uses both look-ahead techniques and CDCL solvers. They also did some of the math on their own ahead of giving it over to the computer, by using several techniques to pare down the number of choices the would have to check, down to just one trillion (from 102,300). Still the 800 processor supercomputer ran for two days to crunch its way through to a solution. After all its work, and spitting out the huge data file, the computer proof showed that yes, it was possible to color the integers in multiple allowable ways—but only up to 7,824—after that point, the answer became no.

While technically, the team, along with their computer did create a proof for the problem, questions remain, the first of which is, is the proof really a proof if it does not answer why there is a cut-off point at 7,825, or even why the first stretch is possible? Strictly speaking, it is, the team used another computer program to verify the results, and the proof did give a definitive answer to the original question—which caused Graham to make good on his offer by handing over the \$100 to the research team—but, nobody can read the proof (or other similar but smaller proofs also generated by computers but which are still too large for a human to read) which begs the philosophical question, does it really exist?

More information: Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer, arXiv:1605.00723 [cs.DM] arxiv.org/abs/1605.00723

Abstract
The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = {1,2,...} of natural numbers be divided into two parts, such that no part contains a triple (a,b,c) with a2+b2=c2 ? A prize for the solution was offered by Ronald Graham over two decades ago.
We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days.
Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

via Nature

Journal information: arXiv , Nature

Feedback to editors

May 30, 2016
This is good new math research show will and thinkthunk

May 30, 2016
Is this really a good uses of a supercomputer? Why not cure Cancer or Alzheimer's, or Parkinson's disease.

May 30, 2016
^ Dear supercomputer, please solve disease. Thanks.

I'm sure it's just as simple as that.

May 30, 2016
So an empirical proof exist and can be checked different way - and philosophy can ask of its existence? Philosophy is not only as meaningless as it seemed, it is ridiculous.

May 30, 2016
The same utterly stupid and boring trolling phrase: 'Is X really a good use of Y? Why not do Z?''

Is that really good use of comment time? Why not do something constructive, like boning up on False dilemma while learning how to refrain from trolling at the same time? https://en.wikipe..._dilemma

[Or if it isn't obvious, supercomputers are used for both math proofs and, more frequently in fact, to study diseases. There are even math proofs that are used in models of diseases - science (and math) is mutually supportive - but that interesting fact would likely blow a troll's boring mind ...]

May 30, 2016
The fact that this proof is ridiculously large is just laziness. There is a set of integers less than or including 7824, that cannot be partitioned. Much smaller than 68 gigabytes or the ridiculous 200 terabyte exposition. It takes less than 32k bytes to list that set. The proof then shows that 7825 cannot be added to the set. (Of course, calling it laziness does not reflect the CPU time required to strip out those values are unnecessary. That might take years of CPU time. ;-)

May 30, 2016
The comment about wasting money that could be better spent is just the same old fallacy trotted, that was used against NASA. They never mention the fact that every dollar spent on the space race earned the USA at least 100 in return.