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?
Indeed. I'm rather confused by the editorial commentary. To put it in terms of the summary regarding a question of color, imagine if someone asked the question, "What color is the sky?" Conjecture: The sky is blue.
Proof? Point an instrument at the sky and measure the light coming from it. Looking at the spectrum of frequencies coming from the sky, it falls into a range of colors that humans would generally associate with "blue."
That's it -- you've "proved" what the color of the sky is, i.e., "blue."
TFS instead starts asking, "But WHY are the frequencies emitted from the sky in the range that qualifies as blue? Why aren't there other dominant frequencies? Why do they fall in a particular range? Have we really proved what color the sky is???"
These are all very interesting questions, but they are irrelevant to the fact that the sky IS blue and one can prove it by measuring the frequency and correlating it with what humans call "blue." Proofs aren't generally about "why," and in fact many concise "elegant" mathematical proofs may be completely non-intuitive about showing why they work -- nevertheless they are considered valid proofs.
These are all very interesting questions, but they are irrelevant to the fact that the sky IS blue and one can prove it by measuring the frequency and correlating it with what humans call "blue."
This is not a mathematical proof but a scientific theory supported by evidence. A mathematical proof, if correct, is always and absolutely true. The major difference is that suppose I did your experiment at night, or at sunrise/sunset, or on a cloudy day? I could get red, black, white or grey for the colour of my sky. All you can do in science is take data, come up with a thoery to explain that data and then test the predictions of that theory under conditions where nobody has tested it before to see whether it works. In your case it is very easy to disprove the theory that the sky is blue.
In fact you can never really prove a scientific theory - all you can say is that it works in all the situations it has been tested under. That's good enough to be extremely useful and to advance our understanding about how the universe works but it is not the same thing as a mathematical proof. This is why scientists spend time confirming that existing theories work in new situations but you never hear of mathematicians checking the pythagorus theorem again to confirm that it still works with new right-angled triangles.