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.
Well, let me take the devil's advocate position for a moment.
Yes, it proves the conjecture, but by relying upon a mechanical process you miss out on something that is required by humans to bring the problem within the grasp of our limited attention spans and working memory: insight. So we know the answer to the conjecture, but it doesn't advance our understanding of the problem and its related problems the way a human proof would.
So you could say it's proof of the conjecture in the sense that it's convincing evidence of the truth of the conjecture. But it doesn't necessarily contribute to mathematical knowledge in the same way you'd expect a traditional proof to. So you could well look at it as a "proof" but in only a restricted sense. This would be fairly typical of the way we use words.
I think one might well be justified in putting computerized proofs into a different class of evidence than traditional mathematical proofs; we might need to distinguish between the two by some kind of retronym.
Post may contain irony: discontinue use if experiencing mood swings, nausea or elevated blood pressure.
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.