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.

[hey!]

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.

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.

Re:Yes.

[GrpA]

42... A very finite number indeed.

And therein lies the problem - Is it possible to demonstrate a proof through brute force?

Re:Yes.

[Anonymous Coward]

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

Re:Yes.

[lars_stefan_axelsson]

Of course it's a proof.

Not so fast. There are several mathematicians that don't necessarily agree with that statement. At least not in its strongest form. (We'll ignore the editor basing their argument on the wrong thing, of course being "satisfying" to a human has little bearing on the "proofness" of a mathematical argument).

In fact, whether computer generated proofs that are too large to check by human mathematicians are really proofs at all is a question that's alive (if not exactly well) in the mathematical community, and you'll find many mathematicians who will sneer at it. This based on the realisation that many so called proofs are wrong. The history of computer generated proofs and verifications in particular being littered with incorrect results (often due to a validation problem, rather than a verification problem, but the latter, due to bugs in the verifier are not unheard of). Hence, the need for some form of human verification. They don't call it "the social process of mathematics" for nothing. Like Jim Horning said: "A Proof is a repeatable experiment in persuasion." Now, if you need another computer to verify the first, you soon end up with a "it's computers all the way down-silly"-type of argument, that doesn't make more pure mathematicians feel exactly warm and fuzzy all over. (Us computer scientist we shrug and get on with it, but that's a different story.)

Re:Yes.

[jouassou]

Fun fact: point scientific equipment up at the sky, and you'll find that it's actually violet. It only looks blue because the human eye is more sensitive to the colour ranges that we call blue than the colour ranges that we call violet. But I agree with your sentiment :).

Re:Yes.

[NotAPK]

"Is it possible to demonstrate a proof through brute force?"

Yes.

Prove that the number of unique permutations of the first 3 natural numbers greater than 0 is 6.

Proof:

1 2 3
1 3 2
2 1 3
2 3 1
3 1 2
3 2 1

QED

Re:Yes.

[NotAPK]

And not only read the source, but re-run the source yourself.

Or write your own program to validate the output of the first.

Even a "simple" proof that sums a long list of numbers would be unfeasible for a human to add up and check, yet we would all feel comfortable writing a program (or a set of programs, each doing the assessment slightly differently) to sum up the numbers and compare the result.

While longer and larger the proof in TFA is not really any different.

Re:Yes.

[tlhIngan]

Is it possible to demonstrate a proof through brute force?

For certain classes of proof, yes.

These classes are ones where the solution space is finite, in which case one can merely enumerate through all the possibilities. Another is where you're proving in general something is true - like in this case. In which case all you need to do is find one counter-example to prove the hypothesis wrong. Which happened here - they simply went through and enumerated the possibilities and checked each and every one of them to see if it meets the conditions.

Re:Yes.

[T.E.D.]

Why would you expect the code for this program to be of such a size that the human mind couldn't grasp and verify

Colloquially, if its bigger than "Hello World", it has bugs. Lots of "Hello World"s have bugs too.

But if you are talking about Formal Verification, that's actually a research topic in CS. Its possible to do, but very expensive. Usually you have to use special compilers designed for that, like SPARK. You ever heard of anyone using SPARK? Well, that should tell you how common that is.

But even then, that doesn't mean you don't have bugs. As Math/CS god Donald Knuth once said of a relatively more simple queuing algorithm: "Beware of bugs in the above code; I have only proved it correct, not tried it."

Computers can't do this for you either. That's part of Computability Theory. You've got the Halting Problem in general, and Rice's Theorem more specific to mathematical transforms. There's a halfway (but not great) discussion of this on this SE Question.

Re:Yes.

[Taxman415a]

On the other side of that coin is what happened to tables of integrals when computer algebra software came out. The tables of integrals in the back of calculus books were considered tablets passed down from on high. Ok exaggerating, but they were considered generally accurate except for typos. When computer algebra software became powerful enough to check them, they were found to be riddled with errors. When checked by hand the computer algebra software was found to correct.

So what's the difference? In the case of tables of integrals, the problem is probably unusually well suited to solving with computer algebra software. Lots of difficult algebra to solve by hand, but relatively few rules to program that, when correct, can be repeated as needed. In large computer generated proofs, there is no easy way to check them to the point that some are basically unverifiable. The only solution I can think of is going back to formal mathematical proof specifications and crunching away until its verified.

Re:Yes.

[HiThere]

What you need to realize is that proofs by humans will also have "bugs". This is why it's important to have multiple independent proofs, if possible, and failing that to have multiple reviewers. But multiple reviewers have been known to overlook the same mistake.

Mathematicians hate the concept, but the foundations of math are not secure. They depend on what humans find convincing evidence. To an extent reproducing the proofs via computer strengthens the proofs, as that reduces the inherent bias. (Everyone has bias in the way they think, and some biases are shared by everyone. Often the only way to discover them is to show that accepting them would cause a more fundamental problem.)

Computers, by using boolean logic, reduce the number of basic assumptions, and therefore are, in principle, more accurate. But they are programmed by humans, who have sloppy thought processes and inherent biases. And sometimes the error correcting codes don't, so there's also hardware errors.

The only really convincing proofs are those that have multiple independent proofs which use different foundational principles.

However, the longer the proof, the more likely it will have an undetected error. This is true no matter whether it's proven by a human or by a computer. There are lots of ways that proofs can be partially checked, but checking for "of course" assumptions is extremely difficult. (Validating the steps of the proof doesn't help if the proof doesn't really prove what you intend it to prove. And that's happened. A notorious example is Euclidean Geometry's parallel postulate [though to be fair Euclid wasn't happy with needing the postulate, and kept trying to find a proof of it]. But it took roughly 2000 years to show that it wasn't really a part of basic geometry, because everyone just presumed it was included.)

Proof?

[swimboy]

This doesn't sound like a proof to me. It sound like they disproved the hypothesis at 7,825. It's kind of like saying that they proved that there are no strings of 8 consecutive zeros in the decimal representation of pi. Well, until you get up to about 172,000,000 digits, at which point there is one.

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:Proof?

[quenda]

Isn't it more like they *disproved* the hypothesis that "there are no strings of 8 consecutive zeros in pi" by finding an example at a given place?

As a non-mathematician - do I understand this correctly?
Expressing a proof that partitioning is possible for {1,2,...n} is simpler - you just provide an example. The hard part is proving that no such partition exists for a given n.
In this case, they both proved the specific cases up to 7,824, and disproved the general case by proving it impossible for the specific case {1,2,...7825} .

The number of possible partitions of that set is 2^7824, which makes the number of particles in the observable universe look rather small, so a brute-force approach is inadequate.

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.

Computer-assisted proofs are proofs

[l2718]

Well, part of the argument is proving that (if implemented correctly) the algorithm actually solves the problem. But in fact this part is redundant -- because what the computer does is actually write out a proof of the theorem.

The point is that while coming up with a proof takes work or ingenuity, verifying the correctness of an proposed proof (written in sufficient detail) is purely mechanical. In other words, you don't need to believe or check anything the researchers have done. You simply need to take the output of their program and use a proof-checker to verify that this output is a valid proof.

For many combinatorial theorems this is the way of the future, and while the submitted may be unsatisfied by a proof which doesn't provide intuition, isn't that better than no proof at all?

Re:Computer-assisted proofs are proofs

[TeknoHog]

Also, consider simple proofs by induction. Besides the actual induction, you need to show that a trivial case works, which is usually plain arithmetic that could be done on a computer. More complicated proofs may require multiple brute-force cases before the actual math can be done. For example, I recall a proof of Bertrand's postulate which first needs individual cases for n < 2000.

It's a bit like physics where you need some concrete system of measurements, a real-world grounding for your abstract work to make sense. If you're doing math with actual numbers, you generally need some numbers to begin with.

Contents of the 200TB proof

[l2718]

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?

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").

Now let $a,b,c$ be a Pythagorean triple (a^2+b^2=c^2 and 1

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.

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.

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.

Re:Contents of the 200TB proof

[XanC]

You can use less than and greater than signs if you HTML-escape them, eg: "&lt;" (<) and "&gt;" (>).

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.

simple proof

[queBurro]

I've got a simple proof of this but it's slightly too large for this comment box. I'll post it laterrrrrrrrrrrrr...

What would Ramanujan Do?

[140Mandak262Jamuna]

What Would Ramanujan

Do?

He will simply calculate all possible Pythagorean triples in his head, write down 7285 in a piece of paper as the "solution" and leave the proof as an elementary exercise to the reader.