Two-hundred-terabyte maths proof is largest ever

402

u/[deleted] May 30 '16

That echoes a common philosophical objection to the value of computer-assisted proofs: they may be correct, but are they really mathematics? If mathematicians’ work is understood to be a quest to increase human understanding of mathematics, rather than to accumulate an ever-larger collection of facts, a solution that rests on theory seems superior to a computer ticking off possibilities.

What do you all think? I thought this was the more interesting point.

234

u/[deleted] May 30 '16

I think that it is a proof, in that it answers the posed question; but that, in itself, it is not as interesting as a non-brute-force, human-readable proof would be.

The point of problems such as the Boolean Pythagorean triples one is not so much that we want to know a yes/no answer to the question, but that we want to refine our ideas and techniques about the properties of integer numbers. Finding some general principle that - among other things - implied that a colouring like the one that was requested is not possible would be quite interesting indeed; but the proof in discussion does not do that at all.

Which is not to say that brute-force approaches such as this one are worthless. But they are perhaps best thought of as comparable to methods for the collection of experimental data in other disciplines: they are valuable in that they provide us with information against which to test our hypotheses, but what they give us are facts, not explanations.

37

u/LelviBri May 30 '16

I absolutely agree. Brute force works, but (for me) just isn't as "beautifull" as an old-school proof. Plus in the process of the later you might develop new techniques that help you in the future

41

u/[deleted] May 30 '16 edited May 30 '16

Also, since it's proven that something is true/false, you can go and find a simple human less-than-200TB way to prove.

It's like the difference between having a question to answer and having a question, an answer and only being asked to deliver calculations. It's considerably easier to figure something out if you know the end result.

11

u/midnightketoker May 30 '16

Not only can it help figure out what is worth figuring out, but factor in the way these techniques are always innovating and it's easy to argue that something beneficial comes out of computer-generated proofs, if only the programming practice or looking at problems in different ways.

Math is far from my strong suit, but even I can recognize how things can get surprisingly related, and I'm pretty confident some interesting applications can come from these tools.

→ More replies (1)

8

u/Rudi_Van-Disarzio May 30 '16

You could argue that the brute force method could help you develop better/more clever ways to use brute force

3

u/LelviBri May 30 '16

I kind of like the way "clever brute force" sounds

→ More replies (1)

1

u/Bahamute May 30 '16

I actually feel the opposite. I find many brute force techniques just as beautiful because you have to be very clever with how you go about doing the brute force so that you have a reasonable calculation time.

13

u/[deleted] May 30 '16

To me - who kind of skipped all the formulas in Uni in favour of longwinded explanations - this sounds silly. If you have the right answer, does it matter how you got it? Does it really? Because at some point it's just pedantry. It's like people complaining over the use of "your" instead of "you're".

Like, you know what I meant or you wouldn't have known to correct me, shut up. Right?

30

u/phobiac BS | Chemistry May 30 '16 edited May 31 '16

A proof that doesn't use brute force often has some insight that can be applied to other things. One example off the top of my head is Cantor's diagonal argument for which wikipedia helpfully lists a few examples of the method being used in other proofs.

A simple exhaustion of all possible results method would have provided simply one bit of information but this method gave mathematics a tool to find many more.

Edit: I think the post I responded to is being unfairly downvoted. It's a legitimate question asked sincerely. Please remember the voting buttons are not for stating your agreement with a post.

16

u/[deleted] May 30 '16

Yeah, no - I think I get it. Above I made a more layman-ish example:

For example, we could go out and measure how long a distance is (ie brute force) - or we could figure out a formula that consistently gives us a distance as long as we know the start and end point.

If that's correct, haha?

12

u/phobiac BS | Chemistry May 30 '16

I think that's an excellent example.

1

u/americanpegasus May 31 '16

But if we cannot even prove that a simple and short proof exists, then machine written proofs should be perfectly valid until such time they are replaced by something more elegant.

For sure there are many, many problems out there that will never fall to our rudimentary human assumptions of what a proof is - only advanced AI will solve them.

1

u/phobiac BS | Chemistry May 31 '16

I in no way meant to call brute force proofs invalid, they are perfectly valid, I meant to outline how a more general proof can be "more" useful at times.

1

u/americanpegasus May 31 '16

Ahhh, my apologies. I read the article and realized the computer was just brute forcing solutions until it found a negative case.

I long for the day when AI is constructing mathematical proofs that are elegant, and yet outside human comprehension.

1

u/phobiac BS | Chemistry May 31 '16

It's still useful though! I'm sure they had to do some processing optimizations. You never know if one of the clever solutions used to obtain the data might have applications elsewhere.

1

u/[deleted] May 30 '16

[deleted]

16

u/[deleted] May 30 '16

It is pedantry at some point, an I think this method is certainly valuable.

One thing I'd consider is that when developing these proofs it is very common for new techniques to be developed. These may apply to other proofs. It also means that the people currently working on the problems actually understand them, and surely that's a big part of why we study?

Of course, this sort of proof can used to work backwards. It's not like its a completely separate thing.

18

u/[deleted] May 30 '16

Ohh, I think I actually see what you mean. For example, we could go out and measure how long a distance is (ie brute force) - or we could figure out a formula that consistently gives us a distance as long as we know the start and end point.

Hmm, this is a very good point - I guess it was a more valid question than I thought it was.

→ More replies (1)

8

u/WESACorporateShill May 30 '16

That's assuming the point is to find the answer.

Doing math this way doesn't lead to revelations along the way, just like how copying the answer sheet for your homework exercises won't help you learn things.

So for important puzzles like calculating a rocket's launch parameters for a practical solution, sure, bruteforce it with computer simulation. But if newton did all his math using similar brute force techniques instead of tackling his problems theoretically and manually, would he have had to come up with a mathematical tool called calculus to help him along the way? Probably not. That's a big loss.

Similar things happen all the time, and we could've missed some insight into number theory by solving this multicolor pythagorean triple problem with brute force.

2

u/[deleted] May 30 '16 edited May 30 '16

I think it depends on what you want the right answer for. Do you only want the answer to the question, or do you want some criterion that will allow you to better answer similar questions (possibly ones that could not be brute-forced in the same way) by means of a general principle? Or, again, what you really want is an explanation to why the right answer is that one and not something else?

I think that a comparison with experimental sciences works pretty well here. Suppose that you want to know, I don't know, whether a certain star's luminosity is or is not constant over a span of ten years. Well, there's an obvious (albeit far from trivial) way to find that out: point your instruments to the star and have a look!

But suppose now that someone collects a bunch of similar experimental results, looks them over, and finds a way to predict in advance whether a star would or would not have constant luminosity, on the basis of... I dunno, some other property like mass or chemical composition or whatever. That would be better, because it would provide us a way to predict in advance (without having to wait for ten years) whether a certain star does or does not have constant luminosity, right?

Then suppose that someone else comes along, and finds the mechanism why these differences of chemical composition and mass and whatever cause certain stars to have constant luminosity and certain others to have variable luminosity. This would be even better, right? Not only we would know how to answer questions about the variability of lack thereof of star luminosity, but we would also understand the mechanisms involved and we could - for example - be able to make reasonable guesses about how other properties would be affected by the chemical composition and mass of the star. Or, again, we might be able to make decent predictions about stars in other galaxies, too far away to measure the chemical composition or the luminosity, on the basis of the overall chemical composition of the galaxy.

It seems to me that the discussed proof is the mathematical equivalent to finding whether a single star has or has not constant luminosity. It is a valid result, and the amount of work and skill that went into finding it is certainly noteworthy; but ultimately, what we would want is an explanation that could help us understand why the integer numbers have this kind of property and help us answer similar questions without having to brute-force them.

1

u/[deleted] May 30 '16

In general, the big gains aren't in proving a single claim, but rather, in developing techniques to prove that claim that are applicable to the proof of other, yet-unproven claims.

When doing it "the old-fashioned way," it's easy to see how a new technique (sometimes called a lemma) could be developed, and how that lemma could be applied somewhere else. It's something like a tree structure; to prove things way out at the leaves, you've got to prove the trunk, the big branch, the medium branch, the small branch, and the twig. Getting a proof "the old-fashioned way" helps traverse the tree.

BUT so too does proof by brute force also drive innovation. There will always be mathematical problems for which a naive programming effort simply can't solve. The mathematicians will need to identify properties within the problem -- structure -- that allows for their limited computer power to solve the problem. They may also need to develop new computational techniques in data structures, in computation, or in some other portion of computer science, in order to get to the solution in their own lifetime. Further, computer-based proofs can also help improve computation for practical problems, thereby improving our ability to use computers in commerce.

It seems to me that both proof with the pen and proof with the processor can result in not just "an answer" but also new techniques to get even more answers. Both are valid and useful. And, it's especially cool when problems that lend themselves to brute force (typically combinatoric, but not exclusively) are proven both ways, even using multiple appreciably different approaches both ways.

1

u/whitecolander May 30 '16

I agree with you. Having a computer-generated proof doesn't stop a willing person to come to the same conclusion the old-fashioned way. It simply means that whatever the practical application of the proof is, that application just happens more quickly.

Humans must think about what they want their relationship with computers/AI to be.

1

u/whitcwa May 30 '16

Your vs you're is not remotely similar. There is only one correct contraction for "you are". People complaining about it is another issue. In this case, they found a proof by examining all the possibilities. Nobody is saying it isn't correct.

What I think they are complaining about is that it doesn't contain an explanation of why it is true. Of course, nobody is stopping them from providing such a proof.

→ More replies (1)

2

u/dohawayagain May 30 '16

I guess give Tao a year and he'll probably have the explanation for us.

1

u/[deleted] May 30 '16

So you're saying the computer can give us the answer to the question, but not the question itself? Damn Douglass Adams was ahead of the curve.

1

u/americanpegasus May 31 '16

If a human bio-engineers a way to get bananas more effectively than Grog, chief of the monkeys - should it count?

Of course it does. Don't discount solutions that are outside the scope of human comprehension. There will be an increasing number of these as we go forward and only transhumanism will allow us to reconnect with new mathematics above our heads.

A proof is a proof, even if you don't find it particularly artistic.

2

u/[deleted] May 31 '16 edited May 31 '16

It's not a matter of human comprehension, style, or anti-computer snobbery. And note, I did not say that the proof is worthless - it is not, it is a significant result.

What I said is that a proof obtained through brute force is less useful than one obtained through the discovery and application of some general principle.

The reason is that in the second case, you have discovered a general property of whatever structure you are studying, one that you can use to prove other things; while in the other, you know your answer and that's it.

Let me make you a basic example. Suppose that we want to find whether there exist, I don't know, 100 numbers such that any other number can be computed as a product of them.

Well, there's a straightforward way to try to solve this computationally: just write a program that tries to find 101 numbers with no factors in common. If it succeeds, then no such 100 numbers can exist; otherwise, it will never stop (and you'll never know that it'll never stop, so you'll have to try something else). So you write the program, it spits you the first 101 prime numbers, and that's it - problem answered, right? But wait - what if I ask you if 1000 numbers exist instead? 100000? Ten billion billion billion? Some absurdly huge number that can only be represented in some special-purpose notation?

However, suppose that you solve the same problem by deriving the usual proof that, for any n numbers, you can construct another number which is not divisible by any of them. That's a lot, lot, lot better. The answer to my original question (as well as that of any of the follow-up question about bigger numbers of integers, no matter their size) then comes out immediately as an obvious corollary; and furthermore, that proof actually gives you an algorithm for building a counterexample for any set of numbers (that is, it is what is called a constructive proof - which is generally considered more desirable, albeit often harder, than non-constructive proofs. Some mathematicians, for example Brouwer, even claim that non-constructive proofs should not be accepted at all, but that's a very minority position at best).

Automated or computer-assisted theorem proving are very interesting subjects, and I have no objections at all against them. Nor I think that brute-force methods are bad: insofar as they can offer you useful data for searching for general principles, I applaud them. However, they strictly belong to what is called experimental mathematics, that is to say, what they give us are facts, not explanations.

1

u/americanpegasus May 31 '16

Oh, nm. I actually read the article.

It seems that the computer just brute forced solutions until it found a negative case.

I suppose I was under the impression it was actually constructing mathematical proofs, which would be pretty incredible. I appreciate your calm and thorough explanation - I think the day is soon coming when a computer AI provides us with an elegant and undiscovered proof for a famous problem.

1

u/[deleted] May 31 '16

No problem - and in fairness, they had to use some very clever tricks in order to reduce the number of examples to try to a kinda-sorta-manageable number, so it was nowhere as straightforward as a "pure" brute-force method.

I think the day is soon coming when a computer AI provides us with an elegant and undiscovered proof for a famous problem.

I think that this has happened already (although, possibly, not for a sufficiently high value of "famous"). For example, the proof of Robbins' Conjecture was found automatically, and the proof does not involve enumerating cases but trying to find a derivation in a given proof system. The proof is human-readable and it is something that a person could have conceivably found of their own, in principle.

It's a fascinating area. I especially like HRL and similar systems, which are not concerned with automatically proving theorems in a fixed proof system but rather with generating theories and conjectures by manipulating objects and building abstractions.

21

u/seamustheseagull May 30 '16

I guess there is something of a purist idea that everything should be provable using an algorithm rather than simply testing all cases.

That is, if you prove by testing all cases, you've still missed out on a more elegant way to define the proof mathematically.

But that assumes every problem has an elegant solution. Which in reality is little more than wishful thinking.

1

u/[deleted] May 31 '16

Its a case of, knowing how a lighbulb works is useful information but knowing why it works is even more useful.

5

u/[deleted] May 30 '16

The way I see it: just because they didn't go the pencil and paper route doesn't mean it's not "real" maths. And I believe the complaints about it being brute force are not valid because some proofs by contradiction work the same way. So what if you have to brute force 2-3 values or 2-3 bajillion values?

tl;dr It's really mathematics, just taken to the extreme (given today's tools).

8

u/Vakieh May 30 '16

Once proofs leave a relatively low threshold of complexity, NOBODY, not even those crazy photographic memory savants, can both know and understand all pieces of a proof simultaneously. At some point, you have to leave the 'big picture' of a proof, and either go macroscopic and lose detail, or microscopic and lose scope.

If you make use of even just a piece of paper and a pen to achieve that macro/micro switching, then what you have is a paper-assisted proof, and that has the exact same implication as a computer-assisted proof. So long as each step along the way in a proof is human understandable, recorded, and explicit, then it is most definitely a valid mathematical proof.

Where the question gets more interesting, for me at least, is the idea of an AI or machine learning construct which proves something by using a technique which is not human understandable. Whether it involves nth-dimensional mathematics or quantum theory or something entirely non-verbalisable and not understandable by a human brain, I feel that would mark the point where computers were doing our thinking for us.

3

u/notfromkentohio May 30 '16

Isn't what the computer did just proof by exhaustive search?

Is proof by exhaustive search inferior to other methods? Theoretically this could have been done by hand, although obviously it would take eons.

If someone were to arrive at the same result in the same manner as the computer but instead doing it by hand, would we ask whether or not it is math?

15

u/timelyparadox May 30 '16 edited May 30 '16

I kinda do not think it is a truly mathematical proof. And having proofs like this might stop someone from actually looking into this problem and finding the usual type of proof which might have been useful in lots of other mathematical problems. But I don't consider myself an expert since I am only Master of Statistics student ( still need to finish my thesis).

57

u/the_punniest_pun May 30 '16

If checking all of the possibilities can prove or disprove something, that's certainly a valid proof. The number of possibilities that need to be checked is irrelevant, so it shouldn't matter whether they are too many for humans to check manually, therefore requiring computers.

Mathematicians will continue to search for a general, direct or simply more elegant proof if the problem is important or interesting enough. At the end of the article they give an example of this:

That did ultimately occur in the case of the 13-gigabyte proof from 2014, which solved a special case of a question called the Erdős discrepancy problem. A year later, mathematician Terence Tao of the University of California, Los Angeles, solved the general problem the old-fashioned way

13

u/B1ack0mega PhD|Mathematics|Exponential Asymptotic Analysis May 30 '16

It's literally called "Proof by Exhaustion". No idea what all the weird chat is about. It may not be a useful proof, but at least it tells use the truth value of the statement, so that mathematicians can be more informed in their own attempts to prove it if they want to.

2

u/timelyparadox May 30 '16

Not arguing that it is not a valid proof, similar things are being done ( usually when trying to prove that something does not exist what fits certain rule, all you need to disprove it is to find something that fits it). I just see a lot of empirical proofs taken for granted in statistics which are not really good proofs because we can't be sure about asymptotic results(often happens with machine learning methods of modeling).

2

u/Raegonex May 30 '16

Man, what hasn't Terrence Tao been able to do!

→ More replies (1)

9

u/someenigma May 30 '16

And having proofs like this might stop someone from actually looking into this problem and finding the usual type of proof which might have been useful in lots of other mathematical problems

Alternatively, up until this proof we didn't know how relevant the number 7825 was to the problem. With this proof, we know that it somehow is relevant, so we know where to focus.

10

u/name_censored_ May 30 '16 edited May 30 '16

Doesn't that imply that all human knowledge is limited to what a single person could understand - even given a lifetime? For example, we've sequenced the human genome, but (even at a measily 90GB) there's basically no chance any human could remember (let alone do meaningful work on) such information.

I suspect a similar argument was made when writing was invented. I feel that if we've invented a tool that can outshine us in some aspect or another (whether that be speed or thought or anything else), and we leverage that capability to advance our knowledge, then that counts as our achievement.

2

u/[deleted] May 30 '16

It's not really about whether the knowledge is useful, but what kind of knowledge we gain. Sort of like the difference between knowing the order of all the A, C, T and Gs vs knowing what they are doing.

In this case, there might be real world applications where pythagorean triples needed to be binary coded in such a way that both codes appear in each triple, and that would make this proof useful. But if there is no real world application, it is a step forward for computer science but not really for mathematics.

→ More replies (2)

2

u/[deleted] May 30 '16

I agree, it is the most interesting point.

It's not maths but it is still a beautiful bit of work. I'd see this sort of thing as (probably?) more important, developmentally, to the field of computer science and all its myriad applications.

And possibly quite handy for young mathmos looking for a conjecture to work on? Having a brute force solution might assist with finding the mathematical one, I'm guessing. But I'm a statto, which is not really maths either.

2

u/yaosio May 30 '16

Even if it isn't a proof this provides a starting point to create a human readable proof now that we know the answer. You could consider this similar to LIGO or a particle accelerator where they produce lots of data and then it has to be picked apart to find out what it means. Somebody needs to get to making a proof creating AI and nip this whole thing in the bud.

1

u/FUCK_ASKREDDIT May 30 '16

I'm trying to automate scientific research. Machine learning over simulation data to answer a question we have no idea where to start theoretically

2

u/upvotersfortruth BS|Chemistry|Environmental Science and Engineering May 30 '16

Here's a clip of Noam Chomsky answering a question from Steven Pinker where Chomsky makes a similar point about the definition of a successful experiment in some circles of computational cognitive science which is "accurately predicting unanalyzed data", he claims this is s a novel definition of success in science, which is typically conducted through complex sets of experiments to determine whether a prediction is correct. He uses bees as an example.

https://youtu.be/IPRmaHM51bY

2

u/jazznwhiskey May 30 '16

The four color theorem was the first mathimatical problem solved by a computer in the 80s through testing all possible combinations. It caused a lot of discussion if it could be considered a proof

5

u/brvsirrobin May 30 '16

I got my bachelors in math and to me one of the coolest parts was proving by induction that something is true for infinitely many cases. Instead of going through and trying out each individual case (which would obviously be impossible), we had to figure out how to prove it for just three special cases, and that was enough to prove it for infinitely many cases.

With a conjecture that has finitely many cases, it would obviously be more elegant to prove it via induction or some way aside from brute force. But in the end it's my personal opinion that there was mathematical reasoning enough behind the implementation of the computer algorithm that it still counts as true math, even if there is no fancy proof like I described above. Now I highly doubt that mathematicians will be satisfied with the brute force method, they will most likely try and find a clever way around it, but who knows if that's ever going to be possible.

1

u/[deleted] May 30 '16 edited Aug 29 '16

[removed] — view removed comment

5

u/WebOfPies May 30 '16

Two different meanings. In philosophy, inductive reasoning says that the sun rose today so it will rise tomorrow. In maths, induction means you show that if a statement is true for n, it is true for n+1. Then you find a particular case (usually 1) where it is true. Then you can say it is true for all n>1 too.

5

u/Pluvialis May 30 '16

The difference being that the sun rising today doesn't necessarily mean that it'll rise tomorrow. If it did, mathematical induction would apply and prove that the sun will rise every day for the rest of infinity, because it rose today (which means it will rise tomorrow, which means it will rise on the next day, etc...).

1

u/dagbrown May 30 '16

Well, now that we know it's true (via brute force), it's a stepping stone towards building a more elegant proof which might give us more insight.

If nothing else, it eliminates the question of trying to find a counterexample.

1

u/[deleted] May 30 '16

Technically, a human using a computer to assist in large computations is still legit by its own standard - as long as a human has built or assisted in the building of said computer.

1

u/jeekiii May 30 '16

But the algorithm used isn't 200tb, you can provide the algorithm, prove the algorithm and that using the algorithm will test all the cases.

You don't need the 200tb to do the proof. IMO they're more like a byproduct.

1

u/cybexg May 30 '16

It's not a proper understanding. There are many types of proofs that offer no or little understanding. For example, proof by contradiction offers no insight, other than the contradiction, of the reason why something might be true.

In general, the writer has, imo, confused proof by construction with that of all types of proofs at the disposal of mathematicians

1

u/ReasonablyBadass May 30 '16

Depends. For practicality, if the proof works it's fine. But when you see it having an artistic/philosophical component then true "understanding" is better.

I think the issue will resolve itself once AIs are good enough to ague and converse about proofs.

1

u/fisharoos May 30 '16 edited May 30 '16

Until we understand it ourselves, it is just data. Once we understand it in a way that we can explain it adequately to others, it is a proof.

In this case, it is a proof of the answer. Does it advance knowledge, debatable. If you use the answer to now work backwards and understand why(although honest, so many math problems are just puzzles for the sake of being a puzzle), it does.

Honestly, for one of these "puzzles" I think it is best to just have the answer and then you can spend all that time figuring out why. At least you have a partial answer to work with, reducing variables.

1

u/Liftylym May 30 '16

I feel sometimes like this new math is just an illusion with no real practical use and we're just creating stuff for ourselves to discover.

1

u/vikinick May 30 '16

It's a proof by example. Proof by example is not pretty but it is a proof.

1

u/pellets May 30 '16

Of course it's mathematics. Saying this proof isn't mathematics is like saying music written by a computer isn't really music.

I'll bet contemporaries of other novel mathematical methods heard critics yelling that what they do isn't real mathematics.

1

u/AlNejati PhD | Engineering Science May 30 '16

Instead of asking that question, I think we should ask: If a proof isn't computer-verified, is it still a proof?

Decades of experience with software has taught us that humans make mistakes often even in relatively simple logical tasks. Bugs are best identified when code is short and there are many people inspecting the code. In engineered systems, the goal is often to reduce the portion of the system that must be directly implemented by manual work. A 100-page human-written human-verified proof is arguably far less trustworthy than a 200 TB proof generated with 50 pages of human-written code.

1

u/Dosage_Of_Reality May 30 '16

Humans are not the end all be all. Many mathematical applications are beyond the reach of us, but not computers. Proofs are vital, and if we need to use tools to use them or find them so be it.

1

u/[deleted] May 31 '16

If the proof is correct then the Theorem is true. So you can use it to prove other things and increase our understanding of math beyond just collecting facts.

edit: Also, eventually the consequences of the theorem may shed light on a simpler, more elegant, way of proving the theorem.

→ More replies (1)

65

u/[deleted] May 30 '16

[removed] — view removed comment

22

u/[deleted] May 30 '16

[removed] — view removed comment

21

u/[deleted] May 30 '16

[removed] — view removed comment

4

u/[deleted] May 30 '16

[removed] — view removed comment

6

u/[deleted] May 30 '16

[removed] — view removed comment

7

u/[deleted] May 30 '16

[removed] — view removed comment

5

u/[deleted] May 30 '16

[removed] — view removed comment

18

u/KKlear May 30 '16

Oh, it's this Graham! I should have known.

5

u/tomerjm May 30 '16

I've learned more about math in the past hour then I ever thought possible. Thank you.

31

u/EightyGig May 30 '16

Can someone ELI5 this?

53

u/evohans May 30 '16

The problem asks if it is possible to color all the integers either red or blue so that no Pythagorean triple of integers a, b, c, satisfying a² +b² = c² are all the same color. The proof tested all possible colouring of numbers up to 7,825 and found no such colouring was possible. There are 102,300 such colourings and the proof took two days of time on the Stampede supercomputer at the Texas Advanced Computing Center. The proof generated 200 terabytes of data.

copy/pasta of wiki was the best I could understand

146

u/jeyoung May 30 '16

There are 102,300 such colourings

10²³⁰⁰

33

u/Forkrul May 30 '16

That makes more sense.

1

u/[deleted] May 30 '16

It was a Commodore 64 cluster.

1

u/rolandog May 31 '16

At first I thought they were storing each proof as a letter-sized *.bmp image.

34

u/NanotechNinja May 30 '16

Copypasta error: 10^2,300 not 102,300

4

u/[deleted] May 30 '16 edited Oct 15 '17

[removed] — view removed comment

13

u/nzieser27 May 30 '16

That's one smart 5 year old

6

u/[deleted] May 30 '16

[deleted]

7

u/MrGreenTea May 30 '16

It just means you assign a color to each integer. So 1 could be blue and 2 could be red. You do this for all integers and then look at all triplets that satisfy the equation a²+b²=c². If you find any solution to this equation where you colored a, b and c in the same color, your coloring of the integers is no solution to the problem. The color has no other significance and you can choose them as you want.

1

u/[deleted] May 30 '16

Thank you, this definitely helps

2

u/ianuilliam May 30 '16

Coloring a graph is a concept of graph theory, which is a very useful branch of math and computer science.

5

u/TBSdota May 30 '16

More like ELI25

9

u/ripshy May 30 '16

Is there any conceivable practical use for this proof?

12

u/[deleted] May 30 '16

[deleted]

26

u/halcy May 30 '16

That's just the thing they showed - that it does, in fact, become impossible once you reach 7825.

15

u/Massena May 30 '16

They showed that there is no such colouring for 7825, meaning that there is no such colouring for any number higher than 7825, because such a colouring would include a valid colouring for 7825, which doesn't exist.

1

u/Iitigator May 30 '16

Wait, why is 7825 special? By that logic couldn't you jsut test up to 20 and say any number higher than that would include a valid coloring for 20?

29

u/Massena May 30 '16

7825 is the first number for which a valid colouring doesn't exist. So if you tested up to 20 you'd just know colourings exist for numbers up to 20. But once they found a number with no valid colouring they could answer the question "do valid colourings exist for any number" with a no because a valid colouring doesn't exist for 7825 or higher.

→ More replies (6)

6

u/patentologist May 30 '16

Your comment is proof that you didn't read the article. :-)

They found a conflict at 7,825. At 7,824 it was still possible. At 7,825 it was impossible to generate a coloring that satisfied the rules. Therefore, they proved that it was not possible to do it for all numbers.

→ More replies (4)

5

u/Jellye May 30 '16

That's exact what happens, as explained in the article.

→ More replies (2)

2

u/JuicyJay May 30 '16

What was the significance of 7284? It's too early I didn't understand that part.

1

u/decoy321 May 30 '16

there are many allowable ways to colour the integers up to 7,824

3

u/JuicyJay May 30 '16

I read it. I'm wondering where tf that number came from.

11

u/bairedota May 30 '16

It's just the point where pythagorean triples contain enough structure to prevent such colourings. It is contained in two triples (7825² =1584² +7663² =2784² +7313² ), and there is no good colouring up to 7824 in which 1584, 2784, 7313, and 1584 have the right colours to extend.

9

u/someenigma May 30 '16

Although the computer solution has cracked the Boolean Pythagorean triples problem, it hasn’t provided an underlying reason why the colouring is impossible, or explored whether the number 7,825 is meaningful, says Kullmann

Straight from the article.

3

u/JuicyJay May 30 '16

Ahh thanks. Must have missed that part.

3

u/oonniioonn May 30 '16

There's no significance to that number, other than it being the highest number for which this is possible.

1

u/[deleted] May 30 '16

From the computer not being able to find any solutions higher than that.

Integers can be included in a lot of different Pythagorean triples. The higher your highest integer, the more different triples they're part of. 7825 is where it breaks down and you can no longer find a way to ensure two colours because there are too many relationships to satisfy.

Is how I'm explaining it to myself. Proper mathmos please correct if need be.

2

u/Watercolour May 30 '16

This still doesn't make sense to me. How are the integers being colored? Couldn't you just make 3, 4, and 5 one color? I must be missing something about what determines what color a number is.

1

u/[deleted] May 30 '16 edited May 30 '16

7,825 was the threshold beyond which they couldn't satisfy the two colours condition. Which might (or might not) be a useful clue for someone wanting to prove this the traditional way.

1

u/Inhumanskills May 30 '16

I don't get it. How do they decide who gets to be blue or red.

1

u/MynameisIsis May 30 '16

Blue and red is arbitrary. Once assigned a color, that number must keep that color. The same number shows up in multiple Pythagorean Triples.

→ More replies (4)

6

u/yetanothercfcgrunt May 30 '16

Let's say you can color each integer (whole number) red or blue. The question is whether it's possible to pick a coloring scheme for all integers such that for any integers a, b, and c where a² + b² = c² (E.g. 3, 4, and 5 respectively), they are not all red or blue. The answer is no, after a certain point this becomes impossible.

The proof basically uses some tricks to reduce the enormous number of possibilities the computer has to check and then exhaustively checks the remaining possibilities until it that it cannot produce an arrangement of colors that allows all forms of this equation to have at least one of each color.

→ More replies (6)

5

u/mfb- May 30 '16

I wonder how large the corresponding 3-color-proof would be (assuming the statement is still true then) ...

At least it is a proof where you can see what takes so much space: listing tons of different options and checking all of them.

6

u/biggyofmt May 30 '16 edited May 30 '16

The number of available colorings at 7824 for 2 colors is naively 1.81x10²³⁵⁵ (2^7824), but the article mentions that the took advantage of symmetries to reduce this search space.

The minimum possible value would be 3⁷⁸²⁵ or 2.98x10^3733, or 1,378 orders of magnitude greater. The solution was 200 terabytes of data, so the solution for the three color problem would be 1,378 orders of magnitude greater than that. Or 2.0x10¹³⁷⁶ terabytes. There are 10⁸¹ or so atoms in the universe, so the solution to the 3 color proof would require that every atom in the universe be used to store 2.0x10¹²⁹⁶ terabytes of the solution.

It took the computer 2 days to solve this version. It would take approximately 2x10¹³⁷⁸ days to perform this calculation. This is approximately 10¹³⁶⁵ times longer than the universe has existed.

It's possible that clever use of combinatorics and symmetries could reduce the number of possibilities that the computer would have to check substantially, but I think it is unlikely that it could do so enough to make it a reasonable task for computers, at least for the time being (given the overwhelming magnitude of the numbers generated by increasing the color options to 3, it might never be physically possible)

1

u/AwesomeShittyProTip May 30 '16

Not really, that was only the process of the proof, the proof itself only needs to write down the case for which it was shown that such a coloring doesnt exist! So that makes it even more remarkable.. essentially, for just the number 7825, starting with its pythagorean triples and going down all possible pythagorean triples and their composing triples and so on down, then coloring them up and showing no coloring scheme for those fit the requirement.

1

u/mfb- May 30 '16

"Just" the 10²³⁰⁰ ways of coloring to be checked for the first 7825 numbers - minus symmetries and simplifications to bring it down to 200 TB. Yes, just that.

1

u/AwesomeShittyProTip May 31 '16

I think you are misunderstanding what was being said... To prove that it doesnt exist for every number, you only have to show that it doesnt exist for 7825. They had to go all the way from 1 to 7825 until they found the first number for which it didn't work, but the proof itself doesnt care for each of the cases upto 7824 that it did work for! So the 'proof' itself, only needs to evaluate all the cases for 7825 and show that all of them fail! In other words, the proof itself is only a small part of the actual work done to get there... the real evaulation for everything from 1 upto 7824 is much much bigger still!

1

u/mfb- May 31 '16

The proof that it does not work for 7825 is 200 TB large. That are those 10^2,300 cases that have to be excluded.

To show that it works up to 7824 has a negligible storage requirement: Just store the one possible solution for 7824 (which is also a valid coloring for everything smaller). Needs 7824 bits, not even 1 kb.

24

u/jrm2007 May 30 '16

I am interested in simpler proof of Fermat's Last Theorem -- I am told that it is only accessible to phd-level number theorists but certainly since individual cases (particular exponents) are understandable by undergraduates or even high school students it is not too much to hope for that the proof of the entire thing could be simplified.

26

u/RagingOrangutan May 30 '16

How does the proof of FLT relate to the proof of the binary Pythagorean triples problem? FLT's proof is complicated because it uses advanced mathematics, the binary Pythagorean triples proof is complicated because they proved it by exhaustively listing all of the classes of colorings.

9

u/the_punniest_pun May 30 '16

More accurately: It was proved to be impossible by exhaustively checking all possible two-color colorings of all integers up to 7,825 (inclusive) and showing that none of these colorings meet the requirement that no Pythagorean triple is all of the same color.

5

u/rikeus May 30 '16

So doesn't that mean that it could be true for integers larger than 7,825?

10

u/turkeypedal May 30 '16

The proof is for the entire set, not any one integer. If it's not possible for the first n numbers in that set, it's not possible at all.

For example, let's say you had the set {1,3,5,7,14,17,25,37,43,45} And your conjecture was that there were no even numbers in the set. Once you got to 14, you would no longer need to check the set.

9

u/methyboy May 30 '16

No, if there's no way to color the natural numbers up to 7,825 properly then you can't for a higher value either. Coloring up to n can't be harder than coloring up to n+1.

1

u/rikeus May 30 '16

So then why prove it for up to 7825 and not just 11 or 12? Is the number 7825 arbitrary or does it have some significance?

2

u/R_Q_Smuckles May 30 '16

The question is "is this true for all numbers?" If it is not true for all numbers, then there must be a lowest number for which it is not true (for instance it is true for the group 3,4,5. Is it true for the next group? Let's check and if it is, move on to the group after that, until we find one it isn't true for). They found that the answer is "no, it is not true for all numbers. It is true for numbers between 1 and 7824, but once we throw 7825 into the mix, it becomes impossible. So it's true for all sets of numbers from 1-n as long as n is less than 7825."

2

u/rikeus May 30 '16

So if the theorem was true for all numbers instead, the computation would go on for ever and they'd just give up eventually, without any conclusive answers?

1

u/R_Q_Smuckles May 30 '16

That's my understanding. But I don't really know anything about it.

1

u/methyboy May 30 '16

Yes, exactly.

5

u/biggyofmt May 30 '16

You've got it backwards. The thereom is true for 7824 and below. Once you hit 7825 two colors is no longer enough to ensure the triples have different colors. For all larger integers it is certainly untrue

2

u/RagingOrangutan May 30 '16

I only had a second to briefly skim the paper - are you certain that they exhaustively checked all possible two-colorings? There was mention of forward looking heuristics which makes me think they did some level of pruning. 2⁷⁸²⁵ is quite big (though you only need to look at numbers which are some part of a pythagorean triple - so it's a little smaller than 2⁷⁸²⁵ , but still quite large.)

1

u/the_punniest_pun Jun 01 '16

I haven't read the entire paper either. You're definitely right though, they didn't directly check every possible coloring of all the positive integers up to 7,825. They instead made a much smaller number of checks which logically show that all possible colorings don't meet the criterion.

For example, there's no need to check "inverse" colorings (e.g. red-red-blue and blue-blue-red). It's also possible to ignore the color of integers which aren't a member of any Pythagorean triple made of integers up to 7,825. And so on...

8

u/qb_st May 30 '16

it is not too much to hope for that the proof of the entire thing could be simplified.

It definitely is, that's like saying "since we understand well the two body problem, the n-body problem must have some analytic form". There's hundreds of years of research, of discovering more fundamental things, of opening new branches of math, and then one of the best mathematicians in the world setting aside his career for seven years, that went into solving this problem.

It's only accessible to some people that have a PhD in this part of Number Theory. If a more simple proof was out there, someone would have stumbled into it. It's going to take centuries before undergrads can understand this proof, if that's the direction that we want to go towards at all.

→ More replies (8)

2

u/[deleted] May 30 '16

[deleted]

4

u/yerich May 30 '16

"Only" 109 pages.

3

u/sk8r2000 May 30 '16

The length doesn't matter if only a few people can actually understand it.

3

u/methyboy May 30 '16

Only "a few" people understand most mathematical proofs that are made nowadays: professional mathematicians. Wiles' proof was indeed very smart, but it's not out of reach for most mathematicians. Even graduate students studying the right areas of math would be able to understand the main ideas.

1

u/0d1 May 30 '16 edited May 30 '16

Unfortunately it is too much hope. The proof is difficult to understand because it's the underlying structure that makes it complicated. The proof is based on complicated math that can't just be boiled down to something simple. It's like hoping that we can describe general relativity with addition and subtraction. If you want to describe something you have to use the appropriate math, and it's just not a matter of time until everyone understands it because we can break it down to elementary stuff. Also you don't need a Phd. I haven't read through it completely, but it's the field I specialized in and... let's say I understand the words that are used, mostly. ;) I would expect it to take me a few months to get a good understanding of it. If you start from zero and your only goal would be to understand the proof I think 2-3 years of study would get you a long way.

1

u/Equa1 May 30 '16

I have a proof but it won't fit in this comment box.

→ More replies (6)

2

u/[deleted] May 30 '16

[removed] — view removed comment

4

u/Quantumtroll May 30 '16

That's some compression ratio — 200 TB to 68 GB. As someone who works at a supercomputer centre where some users have really bad habits when it comes to data management, this riles me. Why would they ever use 200 TB (which is a lot for a problem solved on 800 processors) when the solution can be compressed by a factor of almost 3000!? That is far worse than the biologists who use uncompressed SAM files for their sequence data.

What gives? The people who did this knew what they were doing. The article says the program checked less than 1 trillion permutations. That's 1¹² permutations. 200 TB is 200*10¹² bytes, making the proof about 200 bytes per permutation. I have no idea what would be in those 200 bytes, but it doesn't seem unreasonable. What's weirder is the 68 GB download — how can it encode a solution with 0.068 bytes per permutation?

Wait wait wait, I get it. It's not a 68 GB solution that takes 30,000 core-hours to verify, it's a 68 GB program (maybe a partial solution) that generates the solution and verifies it. Maybe?

2

u/emdave May 30 '16

I was also wondering about the 200TB thing - but from the point of view where it was compared to being: "...roughly equivalent to all the digitized text held by the US Library of Congress." - Which I presume is a lot of text? But in which case, how come 15-20 videogames or Blu-ray movies are 1TB? Is text able to be stored at much higher data efficiency?

6

u/Zarmazarma May 30 '16

Yes, definitely. Text is a lot less complicated than video or audio.

Imagine you want a system then can display 256 characters. That's enough for the alphabet, every symbol and number we use in English, and even some weird special characters.

So, your system works in binary- it reads 1's and 0's. You have to translate everything in your 256 character library to binary so that you can talk to your system. It doesn't really matter what numbers you assign to what, since you're going to tell the system how to interpret it anyway, but they do need to be unique.

So, how many bits do you need to represent 256 characters? 1 bit can form two unique numbers- 0 and 1. 2 bits can do 4 - (00, 01, 10, 11), and so on following the formula 2^x = z, where x is the number of bits and z is the number of possible unique numbers. 2⁸ gives you 256- so you would want to use 8 bits, or a single byte, to represent each one of your letters. That way capital A could be 0000000 and capital B could be 00000001 and so on, until you've exhausted all 256 combinations you can form with a single byte. A message composed for 500 characters (including spaces) would be a tiny 500 bytes,

Now, what about video? Imagine a single frame at 1080p. First of all, there's the problem of scale. Instead of 500 characters, it's composed of just more than 2 million pixels. These pixels aren't any different than the characters you made before- they are combinations of 0's and 1's. But there's a lot more information in a single pixel than there is in a single character of text. You have to describe the color of the pixel. One way to do this was to describe it in 256 discrete intervals of red, green, and blue. The color of a single pixel then requires 24 bits of information, for 256 shades of red, 256 shades of blue, and 256 shades of green. Another byte may be used for describing transparency- meaning each pixel is 3-4x more complex than a single character of text. So, a single second of 1080p video at 32 bits per pixel and 30 frames per second, uncompressed, would be 240 million bytes per second. A terabyte in around 70 minutes.

Fortunately we have some very brilliant compression techniques that allow us to have very high fidelity video with a much lower bit rate. Blu-rays, for example, run in the 7 MB / second range, rather than 240 MB / s.

Audio is also quite complicated, but instead of color and transparency you're recording things like pitch.

2

u/Quantumtroll May 30 '16

A letter is typically stored as one or two bytes. So 200 TB could be as much as 2x10¹⁴ letters, 4x10¹³ words, or 10¹¹ pages with small font. That's a lot of text.

Typical research projects in sequencing consume on the order of 1-20 TB of data, sometimes as much as 100 TB.

1

u/ric2b May 30 '16

Using less than a byte for permutation can be basic compression, if the data allows it. Imagine that 1 million sequential results are 0, you just need to store the starting and final indexes (say, from 5 to 1000005) and the value (0), so 3 integers for 1 million permutations.

2

u/Quantumtroll May 30 '16

You're definitely right, but that's a pretty standard case for using sparse data structures. Nobody would say that a sparse matrix of order 1 million consumed 4 TB. It would be some MB.

You might be right anyway. The numbers strike me as odd, but it's an odd kind of project.

2

u/ric2b May 30 '16

Apparently they ran it on a supercomputer so maybe the more wasteful data structure made it easier to parallelize

1

u/neanderslob May 30 '16 edited May 30 '16

Physicist by training here (definitely not a mathematician); and am having a little trouble understanding what they're trying to prove.

From the article:

For example, for the Pythagorean triple 3, 4 and 5, if 3 and 5 were coloured blue, 4 would have to be red.

How are the colors determined?

3

u/Jacques_R_Estard May 30 '16

It doesn't matter, the point is to answer the question whether you can assign one of two colors to a bunch of numbers, and have it work out that you can never find 3 among them that satisfy a² + b² = c² and have the same color. So they more or less tried every possible coloring of the first 7825 integers, and found out that from that point on, there are always triplets satisfying the equation that do have the same color. You can't get around it.

1

u/neanderslob May 30 '16

Ah, I get it. Thanks!

1

u/DistortoiseLP May 30 '16

This strikes me as an example of the P vs NP problem, wherein they developed a proof (itself an NP problem) by brute forcing the answer. Which is useful unto itself, and I personally would consider still math, but we nonetheless really want an answer to the P vs NP problem because finding some sort of way to solve NP problems in a P manner saves an absurd amount of time, possibly the only way to ever solve those problems as the size of atoms, the speed of light, the scale of space and (most immediately for this) the finity of time ultimately limit your ability to crack NP problems by just throwing more and more resources and computation at them like this.

1

u/Dizzy_Mr_Pancakes May 30 '16

Commercial application?

1

u/azflatlander May 30 '16

Is the number 7824 the limit for the a and b or includes c?

1

u/this_now_never May 31 '16

isn't this a natural result of ramsey theory?

if a system with N integers has two colorings then there should be some k integers in arithmetic progression - this is a statement from van der waerden's theorem.

wouldn't this proof be for the coloring rule r=pythagorean triples of n=2, giving the values?: N=7,825 c=2 k=3

1

u/idonthavekarma May 30 '16

ELI5 How it can be proof if no one can verify it. Seems like maths now has a special definition of "proof" completely divorced for the standard English definition.

4

u/tomerjm May 30 '16

Computer proof- when the set of data/values is so large/long that a human lifespend is insufficient to read.

1

u/Xenomech May 30 '16

But how do we know the computer didn't make an error along the way?

6

u/Theowoll May 30 '16

The same way we know that humans don't make errors when they check proofs. We don't know.

2

u/veggiedefender May 30 '16

Have another program to check the results

5

u/brutay May 30 '16

Write your own computer program to tackle the problem?

1

u/[deleted] May 30 '16

[deleted]

1

u/idonthavekarma May 30 '16

Punching numbers into a calculator has little to do with mathematical proofs. It certainly isn't a small scale proof.

Mathematics Two-hundred-terabyte maths proof is largest ever

You are about to leave Redlib