Four Color Theorem

[worzel]

I've addressed them several times now. The code can run consistently on several platforms; it can also run consistently incorrectly. We are unable to know that such code contains no error. Yes, mathematicians could check the code easily, if you say to them, "We think this is the specific microcode error that exists." However, if you instead say to them, "Verify that no error whatsoever exists in this microcode", then it's no longer so easy to verify. If it was so easy to verify, why did Intel have such an error three times? And if they had it three times, how do you know that there is not a fourth example of it?

Remember that the microcode is not part of the proof, it does not port with the code from one platform to another. A mathematician checking the code is checking the algorithm that does port, not the microcode of each chip it is ported to. The algorithm has not only been checked, but improved and reimplemented in different languages, and then run with equivalent output.

If I were charged with programming this task, I would have the code output how it dealt with each configuration, not just a "yes" or "no". If the output matched on different architectures then the chances of there being an error in the microcode of each chip used in just such a way that it affected each execution of the code on those different platforms in just such a way as to produce identical output is astronomically small. I'm sure the smart people who have done all the checking did something at least as thorough, why wouldn't they? Finding a genuine error in the proof would gain one far more notoriety than confirming it.

If you cannot accept that computer participation in the Four Color Map Theorem invalidates the solution, then there is not point in my continuing to demonstrate a proof here that avoids the problem.

If you won't present your proof then there is little point carrying on the discussion. An elegant proof would obviously be highly desirable whatever one thinks of the current proof - sounds to me like you're trying to weasel out because you know your proof is flawed. If I'm wrong, prove me wrong, present your proof!

[peter eldergill]

Could it be argued then along the same lines that Euclidean Geometry is not valid either because he based it on "postulates" (or assumptions)? Like parallel lines never meet and others (Sorry, I can't remember...I thought there a five postulates he had, some of which have been shown to be equivalent?

I agree with Worzel about a traditional proof. This would be fantastic, but since none exists (until Maddad supplies us with one, that is :surprised ), I will accept the computer proof.

Pete

[montebianco]

Could it be argued then along the same lines that Euclidean Geometry is not valid either because he based it on "postulates" (or assumptions)?

Won't get far without postulates

Like parallel lines never meet and others (Sorry, I can't remember...I thought there a five postulates he had, some of which have been shown to be equivalent?

Some info here.

http://www.health.uottawa.ca/biomech...aws/euclid.htm

There have been attempts to prove that the fifth postulate is redundant, but it is now known that this cannot be done, and systems of geometry in which the fifth postulate is false have been developed.

I agree with Worzel about a traditional proof. This would be fantastic, but since none exists (until Maddad supplies us with one, that is :surprised ), I will accept the computer proof.

Pete

It fits on a couple of sheets of paper? If such a thing exists, then who cares about a computer proof.

[peter eldergill]

Quote:
Originally Posted by peter eldergill
Could it be argued then along the same lines that Euclidean Geometry is not valid either because he based it on "postulates" (or assumptions)?


Won't get far without postulates

That's what I was trying to get at I think, don't we have to assume that the computer works well enough to prove this? I would trust the word of the chip designer if that's their claim (i.e. I will take the word of the expert)

Pete

[peter eldergill]

Some info here.

http://www.health.uottawa.ca/biomec...laws/euclid.htm

There have been attempts to prove that the fifth postulate is redundant, but it is now known that this cannot be done, and systems of geometry in which the fifth postulate is false have been developed.

Are Hilbert's spaces then more complete than Euclids (in terms of missing assumption in the axioms?)

Pete

[montebianco]

That's what I was trying to get at I think, don't we have to assume that the computer works well enough to prove this? I would trust the word of the chip designer if that's their claim (i.e. I will take the word of the expert)

Pete

Well, we would have to assume that, but I think that's the issue here. At least one person here objects to this as an axiom (I don't particularly like it myself )

[montebianco]

Are Hilbert's spaces then more complete than Euclids (in terms of missing assumption in the axioms?)

Pete

It would appear so, but I'm way out of my element here. A Hilbert space to me means something rather different (an infinite-dimensional vector space with an inner-product, maybe some other requirement that I've forgotten)

[peter eldergill]

I thought Hilbert Spaces were finite dimensional (usually). Or perhaps hyperdimensional? Ha!

I recall a geometry prof starting many theorems with "Let V be a finite dimensional Hilbert space with an inner product", but I never even knew that Hilbert had more accurate axioms for geometry

Pete

[peter eldergill]

Well, we would have to assume that, but I think that's the issue here. At least one person here objects to this as an axiom (I don't particularly like it myself )
Reply With Quote

Isn't a large chunk of chaos theory (dynamical systems) done with the aid of computers?

Should we also abandon all of that?

Pete

[montebianco]

Isn't a large chunk of chaos theory (dynamical systems) done with the aid of computers?

Should we also abandon all of that?

Not of any particular interest to me, but why do you seem to suspect that I feel it should be abandoned?

[montebianco]

I thought Hilbert Spaces were finite dimensional (usually). Or perhaps hyperdimensional? Ha!

I don't usually think explicitly in Hilbert space terms, but I do recall reading a book (it was March 2003, I remember where I was when I read it and I've only been there once) which defined them as necessarily infinite-dimensional. I also recall thinking that that was odd...but certainly, the space of L-2 integrable functions on the real line is a common example of a Hilbert space, and that's infinite-dimensional.

I recall a geometry prof starting many theorems with "Let V be a finite dimensional Hilbert space with an inner product", but I never even knew that Hilbert had more accurate axioms for geometry

I didn't either. He did quite a lot though, including, I think coming up with the first solution to the field equation of Einstein, even before Einstein did - but perhaps I am mistaken, perhaps it was derivation of the equation itself. Or maybe I'm completely misremembering...

[HenrikOlsen]

(Sorry, I can't remember...I thought there a five postulates he had, some of which have been shown to be equivalent?

He had 5 postulates.

1. You can draw a straight line from any point to any point
2. you can continue a line to infinity
3. you can contruct a circle with any center and any radius
4. all right angles are equal to one another
5. If a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if extended indefinitely, meet on the side on which are the angles less than two right angles.

None of these can be derived from the others.

People had been trying to derive the 5th from the others for millenia until it was shown that it couldn't be done by generating internally consistent geometries using other propositions

[peter eldergill]

Not of any particular interest to me, but why do you seem to suspect that I feel it should be abandoned?

I mentioned this due to the recent discussion about possible flaws in the computer processors

Pete

[hhEb09'1]

I don't usually think explicitly in Hilbert space terms, but I do recall reading a book (it was March 2003, I remember where I was when I read it and I've only been there once) which defined them as necessarily infinite-dimensional. I also recall thinking that that was odd...but certainly, the space of L-2 integrable functions on the real line is a common example of a Hilbert space, and that's infinite-dimensional.

Hilbert spaces can be infinite dimensional, but there are finite dimensional Hilbert spaces (cite).

[Maddad]

Remember that the microcode is not part of the proof

It most certainly is! The person running the progrogam interfaces to what the programer wrote. That sits on top of the program that compiled the program, which in turn rests on the operating system. The entire shooting match talks to the microcode, which means that the microcode is the most fundamental part of the proof offered by a computer program.

Porting to a new chip bring up a new microcode set, to be sure, but now you're needing to examine the validity under multiple systems for errors of unknown quality. Not only have we not positively researched the first microcode set; we sure as shootin' haven't compared the results against a second set. While much of the microcode is identical from one manufacturer to the next, there are differences if for no other reason than to avoid copyright infringment issues. Howsomever, because the ultimate job of the microcod of one processor is essentially identical to the job of another, it must be very close. If errors exist, they may be conceptual errors that both systems share.

Worzel, you're a smart guy, and I'm not telling you anything you don't already know. You have to be operating on an emotional inability to deal with the issue to keep missing such a basic issue.

there is little point carrying on the discussion.

I agree. If we cannot get past these basics, then the logic reversals in the proof will indeed be too confusing to understand.

Could it be argued then along the same lines that Euclidean Geometry is not valid either because he based it on "postulates" (or assumptions)?

No sir.

That's what I was trying to get at I think, don't we have to assume that the computer works well enough to prove this? I would trust the word of the chip designer if that's their claim (i.e. I will take the word of the expert)

Establishing oroofs is not about accepting the word of an expert.

[montebianco]

Hilbert spaces can be infinite dimensional, but there are finite dimensional Hilbert spaces (cite).

That's what I would have thought, but after the post I made above, I even went and checked my book, and it does indeed say necessarily infinite-dimensional! I remember thinking this was odd at the time.

Arg, now I have to check again because I can't remember who the author is...

[montebianco]

I mentioned this due to the recent discussion about possible flaws in the computer processors

Pete

I'm not suggesting abandoning anything. I just don't like adding "The computer works properly" to a list of axioms. In a rigorous logical system with a well-defined notion of truth and falsity, then the axioms determine the truth or falsity of a statement, independently of any proof. The proof tells us whether it is true or false, but it was true or false before we came up with the proof; we just didn't know it. I just wouldn't want to add "The computer works properly" to a list a fundamental axioms, anymore than, for a proof done without a computer, I would want to add "The person who wrote the proof and the people who have checked it didn't make any mistakes."

This was the intended meaning of my earlier statement.

[Grey]

I agree. If we cannot get past these basics, then the logic reversals in the proof will indeed be too confusing to understand.

Regardless of what Worzel thinks, I'd be very interested to see your proof. Either it has a flaw in it, which will be interesting to track down, or it's valid, in which case I'd fly out to see Pace eat his hat.

[peter eldergill]

Bring it on! Then I can pretend to understand it!

Pete

[hhEb09'1]

If you're so willing to spring for the fare, I'd fly there

[worzel]

Worzel, you're a smart guy, and I'm not telling you anything you don't already know. You have to be operating on an emotional inability to deal with the issue to keep missing such a basic issue.

I'm afraid you're missing a very basic point. The microcode on different architechtures is completely different. The same program written in 'c', say, would even compile to different machine codes on different architectures - how could they possibly share microcode? If the same program written in a high level language is compiled for, and executed on, differing archictures and produces identical output, then if that output is quite verbose the odds of there being a microcode bug on each architecture which affected the outputs identically is astronomically small. Moreover, the algorithm has been reimplemented in different languages, and improved algorithms have also been developed. Guess what, they all confirm the result.

I put it to you, Maddad, that you have an emotional inability to let go of what was a temporary doubt with the current proof because you wish to cling on to your fantasy that you are the first to prove it.

I agree. If we cannot get past these basics, then the logic reversals in the proof will indeed be too confusing to understand.

Nonsense. The only thing stopping us from discussing your proof is the lack of your proof. As both I and Grey have stated, what I think of the current proof is irrelevant to your proof. You claim to have come up with it while stil at school and claim that it fits on a sheet of A4 so I am pretty confident that my feeble mind can deal with it. But even if it is beyond me, I can assure you that both Grey and hhEb09'1 are more than up to the task and are both eager to see your proof.

[Celestial Mechanic]

The problem with a computer proof is not philosophy; it's that we are unable to know, to the level necessary to claim proof of the Theorem, that the computer did in fact perform it's calculation correctly. Maybe you quickly passed over my original reasoning, but we are unable to know that the code is correct because we are unable to be sure that the microcode in the processor is not flawed. Remember, we have not one, but three prior instances in which this microcode later turned out to be defective.

I've addressed them several times now. The code can run consistently on several platforms; it can also run consistently incorrectly. We are unable to know that such code contains no error. Yes, mathematicians could check the code easily, if you say to them, "We think this is the specific microcode error that exists." However, if you instead say to them, "Verify that no error whatsoever exists in this microcode", then it's no longer so easy to verify. If it was so easy to verify, why did Intel have such an error three times? And if they had it three times, how do you know that there is not a fourth example of it?

But what assurance do we have that mathematicians have performed their calculations and logic correctly? In the case of the four-color theorem, there was a proof published by Kempe in 1879 that stood for 11 years before Heawood gave a counter-example and re-opened the problem in 1890. The chances are very good that your proof likewise has a small logic error, something easily overlooked. No one will ever know until your proof is submitted to review.

As for your three examples, I know that one of them was in floating-point division (something not likely to be used in a combinatorics problem like the four-color theorem), but I don't think the others were in arithmetic. (But please correct me if they were!) I think the others were technical things that affected operating system functionality but not arithmetic. The odds of a computational bug is very small precisely because so many results are known precisely and we can verify the results we get.

[jfribrg]

One thing I haven't seen mentioned is that there is ongoing research into mathematical proofs of program correctness. I haven't dealt with it since grad school, so I can't give an example until I dig up my old books on the subject, but in general it is possible to prove that certain types of programs are correct. The problem here is that it has been proven that real-time systems cannot be proven correct, so the issue of the microcode becomes the main theoretical stumbling block. I have not been able to find any references to prove the correctness of the 4 color theorem ( I didn't look too hard either). I think this can be done in 3 steps:
1) Prove that the algorithm is correct ;
2) Prove that the RISC implementation of the program matches the algorithm
3) build a special purpose RISC computer that runs the program and nothing else. Specifically, this computer can have no interrupts, and the only output is a binary value. This last step may seem far-fetched but is necessary in order to complete the proof.


I am not sure if the theory of program correctness proofs has matured enough to handle something as complex as the 4 color theorem, but I don't see any reason why it couldn't be done, especially if we use an automated theorem proving program to do step 1 for us. That may sound like a circular argument (using a computer to prove that a computer proof is correct), but it isn't since the ATP output can be hand checked.

I know this is a rambling post, and I will make additional posts in the near future to clarify these ideas.

[Maddad]

Regardless of what Worzel thinks, I'd be very interested to see your proof. Either it has a flaw in it, which will be interesting to track down, or it's valid, in which case I'd fly out to see Pace eat his hat.

Ok. I told myself that I'd post it if there was one person interested. You're it.

Our initial world will be a limited two dimensional surface--a sheet of paper. We will arrange territories so that they do not border each other directly, but rather we represent their border by drawing a line to connect them. A border between two territories may not cross the border between another two. We'll represent the territories by simplifying their shapes to a circle. When we add the first territory to the new map, there is only one possible place to put it. On the map.

Grey, are you Ok with my reduction of territory shapes to circles and representing borders between them with connecting lines? I don't know if I need more explanation here or not.

[hhEb09'1]

Grey, are you Ok with my reduction of territory shapes to circles and representing borders between them with connecting lines? I don't know if I need more explanation here or not.

I don't think there should be any problem with that. I think that's actually the usual way of representing the regions.

[Grey]

Grey, are you Ok with my reduction of territory shapes to circles and representing borders between them with connecting lines? I don't know if I need more explanation here or not.

That's just fine. As Pace pointed out, most mathematical treatments of the question generally use the same method.

[snarkophilus]

You can do simple tests to see whether or not the basic electronics function properly. It is not hard. I remember doing it in a second year hardware course. This is always done at the factory, of course.

Of course, you might argue that random data corruption might skew your results. This happens rather frequently, in fact. Little static discharges in the air and across circuit boards change data all the time. However, we have error-correcting mechanisms built into machines that make the chances of an error in a processor not being picked up very small indeed. Also, these errors are not reproducible, and are weeded out when you run the programme again.

Or maybe your OS is bad, and it changes your data in some way. Run under two OS's, because there is almost no way that such an error would exist in two separate products. If you're really paranoid, build your own OS, one whose correctness can be proven (and this can be done).

All that's left is the algorithm and the logic of the proof itself, which have been rigorously checked.

Look at it this way. Treat the computer as a scientifically studied object. If, after determining that the chance of getting bad results is less than, say, 10^-12 (which is much worse than data corruption going undetected at the hardware level, and much worse than the same corruption happening the same way on two machines), you can't trust your computer to do its calculations correctly, then you can't trust anything. You can't trust pictures you get from Hubble. You can't trust the clock on your wall. You can't trust that the food in your stove is being cooked at a high enough temperature, or that you are even reading this right now and not imagining it. All of those things have errors worse than those of a properly built computer. Very smart people have thought of these things, and they've built in safeguards.

All in all, a proof being false as a result of massive, widespread machine failure is far less likely than my going insane and just imagining that the proof was false. I'm willing to go out on a limb here and say that it's probably fine.

(As an aside, the Pentium arithmetic problem was a big deal for a couple of people I know... they did not know about it prior to buying machines, and ended up having to re-run several thousand hours of simulations. So now they build pretty comprehensive test programmes to run on any machine before using it for scientific purposes.)

[Maddad]

Snark
That approach works if we are looking for the kind of error the system exhibits. If it has a different kind of error then we would not be successful.

Grey
Ok. When you introduce the second territory on the map, there is also only one possible place you can put it. Somewhere else. I like to keep the separation between them at least several territory diameters, but that is only an issue of taste. If you make the distance much less, then as your map becomes triangular it becomes unnecessarily crowded when you add another internal territory. If you make the disconnection too great, then the diagram can become ungainly. I also like to think of the line connecting the two territories as slightly thicker than a simple pencil line, but again this does not affect the outcome of the problem whatsoever. Thin works just fine.

What you wind up with is a dumbbell appearance. Two circles separated by a bar. I think of the dumbbell as being horizontal, roughly centered on the page, but it will function identically if you draw it vertically or even diagonally.

Ok, before we introduce our third territory, do you have any questions?

[Grey]

Ok, before we introduce our third territory, do you have any questions?

Nope. Looks good so far.

[jfribrg]

I recall a few years ago someone an empirical demonstration of the 4 color theorem by using a "chemical computer", using amino acids. By combining different amino acids in a solution, if four colors were not sufficient, then certain types of proteins would be produced. After combining them, no such proteins were found. Its not exactly a proof, but since many trillions of molecules were used in the solution, the correctness of the theorem is very compelling. Combine that with the other proofs and it becomes very difficult to argue that the theorem is wrong. One may still argue that it is not rigorously proven (others would disagree), but to argue that it is false is a very difficult position to support.