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?

Comments

Yes.

[Samantha Wright]

Of course it's a proof. Who taught you what the word "proof" means? Perhaps you were looking for "satisfying answer," dear editor?

Re:Yes.

[AthanasiusKircher]

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.

Re:Yes.

[Donwulff]

It's proof, but the problem is the measure of "largest math proof ever" is dumb. I could let a computer (or preferably a cluster) generate proof that every natural number below 200 trillion is followed by another, and there are no gaps, and it would easily trump that as the "largest math proof ever". What's that you say, it's not the simplest proof? True, but my algorithm just didn't hit on the simplest proof yet... Or if you prefer, I can generate proof of the exact number of primes below 200 trillion, it would beat that record by far and as far as currently known, have no simpler proof. For that matter, the Great Internet Mersenne Prime Search is constantly generating proofs that, if written and dumped out sequentially, would beat the pants off this record. But I hope we're not (or shouldn't be) merely competing for "the largest waste of computing power ever" :)

Re:Yes.

[K. S. Kyosuke]

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.

I'm not sure how enumerating a finite set and demonstrating that a property holds for all its elements (or conversely, that it doesn't hold for some of its elements) doesn't constitute "a traditional proof". Dealing with finite cases by enumerating them seems perfectly traditional to me.

Re:Yes.

[thinkwaitfast]

IBM Blue Ice supercomputer 325.40 kW x 48hours x 0.10/kwh = $1,561.92.

Re:Yes.

[U2xhc2hkb3QgU3Vja3M]

Dude, we all know that if you keep digging these "why" questions, you'll just end up with 42.

Re:Yes.

[HiThere]

That's not even true of many traditional proofs. Some traditional (i.e., by humans) are long enough to require weeks to months of study, as well as years to produce.

This is more extreme in that nobody can reasonably go over that much proof, no matter how dedicated they are, but in principle it could be done by overlapping teams of people. It won't be, because people don't doubt it sufficiently. Various people will look at various parts of the proof. But it *could* be done.

There's one math proof that's been published for over a year (forget what it's about, or how much over). It's by one mathematician, not by a computer, but it was developed over a decade or so, and he developed some eccentric tools that aren't widely understood, so verifying the proof requires significant work, and hasn't been done. Will it be done? Is it as trustworthy as a proof by a computer that also hasn't been gone over in detail by lots of (other) mathematicians?

The problem isn't just computers, it's a degree of complexity beyond what most professional mathematicians are prepared to deal with. And it's showing up in several places around the edges of various fields.

THIS belongs on Slashdot

[x_IamSpartacus_x]

This is absolutely news for nerds. Please post stories like this one and fewer "Why Trump/Clinton are lizard people" stories.

On topic, what is the content of this 200tb proof? Is that just a text file where each character is a bit? How many libraries of congress is this proof?

Whatever the content, congrats to this team of mathematicians.

Re:Proof?

[l2718]

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.

Re:Contents of the 200TB proof

[l2718]

Sorry, the system ate my "less than" signs. Here's a corrected version.

1. Consider the integers between 1 and 7285. To each integer i assign a boolean variable P_i. These variables encode the partition of these integers into two classes (think of P_i as encoding the statement ""the integer i belongs to the first class").
2. Now let $a,b,c$ be a Pythagorean triple (a^2+b^2=c^2 and each is between 1 and 7285). Construct the boolean expression Q_{a,b,c} = (P_a & P_b & !P_c) || (P_a & !P_b & P_c) .." (disjunction of 6 clauses each being a conjunction of three terms) describing the 6 ways in which a triple can be non-monochromatic). So Q_{a,b,c} encodes the assertion "the integers a,b,c are not in the same class" by writing out the 6 ways in which a,b,c can belong to two classes without all belonging to the same class).
3. Finally, the claim "every triple is not monochromatic" is obtained by taking the conjuction of the Q_{a,b,c} over all triples (a,b,c) as above. It's a huge boolean expression and the goal is to show that it always evaluates to FALSE (in other words, that for any boolean assignment to all the P_i), the huge conjugation always takes the values.
4. The proof works by manipulating this boolean expression: it has 200TB of instructions on how to manipulate this huge boolean expressions step-by-step in ways that obviously don't change its truth value, so that at the end one of the clauses in the conjunction simply reads "FALSE", making the whole expression indeed universally false. A computer program discovered this list of manipulations, and a separate (much simpler) program can easily verify that the manipulations are of the right kind (they don't change the truth value) and that at the end of the manipulation you get a clause saying FALSE.

Mathematical Proof != Scientific Theory

[Roger W Moore]

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.