Slashdot Mirror
Computer Generates Largest Math Proof Ever At 200TB of Data (phys.org)
An anonymous reader quotes a report from 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. 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^2 + b^2 = c^2, 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. 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. 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? Does it really exist?
They proved that in every partition of the positive integers into two classes, one class contains a solution to the equation $a^2+b^2 = c^2$. The method of proof is by showing this is already two for any partition of the interval {1,2,...,7,825} into two classes.
This is not entirely surprising; probably there will eventually be quantitative bounds showing that if you colour the integers in {1,2,...,N} in two colours then there are at least f(N) monochromatic Pythagorean triples for some increasing function f(N). Then 7,825 is the first N where f(N)>0, that's all.
I do agree with you that Graham probably expected a proof of the quantitative type rather than a computer search, because many other Ramsey theory problems have quantitative solutions, but there's nothing wrong with starting with a computer search.
IBM Blue Ice supercomputer 325.40 kW x 48hours x 0.10/kwh = $1,561.92.