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.

[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.

[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.

Re:Yes.

[Anonymous Coward]

It is upon the asker to define what would qualify as blue. Otherwise the problem is underspecified.

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:THIS belongs on Slashdot

[PsychoSlashDot]

This is absolutely news for nerds.

I'm going to play devil's advocate and point out that this story literally boils down to "someone used a computer to do what computers do."

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.