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 math problem 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: a² + b² = c², 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 supercomputer would have to check, down to just one trillion (from 10^2,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?

© 2016 Phys.org