--0__=Lo2ie8JCvFyKTEo9MdGo69gDqCO5GtVIFv0w67il0qMKPs8f5wNe3wmI Content-type: text/plain; charset=us-ascii Content-Disposition: inline From: Tom Gray@MITEL on 03/12/2001 08:18 AM He controversy wasn't that the computer examined all possible examples since this is essentially what a mathematical proof is. Someone examines a problem and classifies all possible types of solution. That person then proves that a property holds for every one of those classifications. In the case of a proof by induction, there can be an infinite number of these classifications, one proves that it is true for the first and then proves if it is true for n it must be true for n+1 and so it is true for all. The issue as I remember it was about two things: a) the exact problem was not that interesting. The interest was in the development in mathematics and mathematical understanding which were going into solving it. Many workers had trued to restrict the number of possible map classifications over the years to a tractable number to some success. The program short circuited this process and just analysed several hundred thousand possible cases which covered all possibilities. There was little mathematical benefit to this. b) the proof came in the form of a computer program and no one could be sure that there were no bugs in the program. A mathematical proof is supposed to be a mechanical statement that in principle someone could follow without any insight. Perform each operation as detailed by the proof and the result is inescapable. No one could possibly do what the computer did so this type of justification for mathematical proof was lost. The proof was verified by the development of an independent computer program which redid the checking. This was a new form of justification. What Cantor proved is that there are multiple kinds of infinity. To be precise he proved that there a an infinite number of transfinite numbers. In particular he proved that the cardinality of the natural numbers ( these are the integers or counting numbers from one up so 1, 2,3,4 ... and cardinality is the number of them this transfinite number is usually denoted by the Hebrew letter Aleph) is less than the cardinality of the real numbers (all numbers of decimal placeswn whicfh is called teh continum and denoted by the small letter c). He did this by using an argument that showed that no matter how many real numbers were placed in a list (i.e. matched with the counting numbers so there would be a first real, a second real and so on) a new one can be created that is not in that list. Indeed between any two real numbers there are more real numbers than there are natural numbers. To be even more mystical the cardinality of the set of all real numbers between any two real numbers is the same as the cardinality of all real numbers which to me seems to be amazing. Infinities are difficult concepts and many people objected to these results as unjustified especially since the proof that Cantor developed - the diagonal proof - relies on operations on an infinite number of operations. However by examing this issue, Cantor developed set theory which is a fundamental part of logic and mathematics. Tehe is a widespread industry now in computer science deaprtments using mathematical proofs to show the correcness of computer programs. Despite teh claims of its proposnts this method has had little practical importance. However it does indicate that there can be no possibility of a computer program ever correctly claiming that it has found a proof that differs from a mathematiocal proof. Indeed the concept of program as a set of steps to produce a result comes from mathematics. [log in to unmask] on 03/12/2001 07:23:56 AM Please respond to [log in to unmask] To: [log in to unmask] cc: (bcc: Tom Gray/Kan/Mitel) Subject: Re: OFF TOPIC - Map coloring In a message dated 3/11/01 7:27:31 PM Eastern Standard Time, [log in to unmask] writes: > In Dublin I read part of the book on the history of the map-colouring > problem and how it was solved, which was really interesting to read - it > was one of the first proofs in which computers played a great part and > hence it was and still is very controversial. Arwin, What's the book? The reason the proof was controversial is that it isn't actually a "proof" in any logical or mathematical sense. Just a brute force examining of all examples the computer could think of, and no proof (or way of proving) that the program was actually sufficient to test "every" possible example. Personally, I think the map-coloring problem is a design problem, not a mathematical problem, and that's precisely why problems arose in trying to formulate a solution in mathematical terms. One question is whether there are criteria for identifying a mathematical problem as opposed to some other kind of problem. If these criteria exist, I sure don't see where they are, and the envelope can't be pushed to include any question with a numerical answer. There's no provable mathematical formula, for example, that allows anyone to determine what numbers are used on the license plate for my car. And the question isn't actually a mathematical question, even though the answer can be expressed in numbers. One can get an answer by checking the motor vehicle records. But looking up a number on a list isn't the same thing as constructing a mathematical proof...unless mathematicians are willing to broaden their standard of what constitutes a mathematical proof so that it includes all the "trivial" proofs that seem to be ignored at present. I think Cantor developed some proof that there can't be any highest possible number or any end to the number series...which tends to validate the common sense observation that no matter how large a number is, one can always add 1 to it. So why should we believe a computer that erroneously tells us that there actually is a highest possible number...this being the highest number that this particular computer can express given its limitations of memory and technology? In any case, I'd like to see the actual program for supposedly "proving" the four color theorem, which I think came from U of Illinois. Was it reprinted in the book you read? It's supposed to be teribbly long, rather than a relatively short program that's used recursively. I'd like to see whether what made it so long is an attempt to define "every possible" situation. There was a period, you know, when an attempt was made to demonstrate that computers can do all kinds of things they aren't actually capable of doing. One engineer was claiming a computer could make Mondrian paintings, and another started that stupid "the Mona Lisa is Leonardo in drag" stuff. Here, the arguments were set forth in relatively brief articles. And when one finished reading the articles, one realized each was written by a person who didn't know a thing about art, and therefore didn't know how to interpret the data. In the 4-color theorem, too, it seems to me from what I've read that the programmers skipped too many steps. Starting at square one, the first job is to program a computer to construct mathematical proofs. Until that's been accomplished, a computer isn't able to construct a mathematical proof of anything. And this of course is the borderline question that I hope is being considered in AI. What's the limit to what a computer can do? And what problems can only be solved by a sentient being? All that to-do about computers playing chess is far from persuasive, because chess has a finite number of possible moves. What about programming a computer to write a recipe book, with some assurance that the receipes will be superior to those a human being might develop? Here, it's a tougher problem, because more is involved than shuffling numbers, which is all computers can do. But, as above, I think the main problem with any computerized "mathematical proof" of the four-color theorem is that one can't skip the necessary step of developing a program capable of constructing mathematical proofs. pat --0__=Lo2ie8JCvFyKTEo9MdGo69gDqCO5GtVIFv0w67il0qMKPs8f5wNe3wmI Content-type: text/html; name="att1.htm" Content-Disposition: attachment; filename="att1.htm" Content-transfer-encoding: base64 Content-Description: Internet HTML PEhUTUw+PEZPTlQgRkFDRT1hcmlhbCxoZWx2ZXRpY2E+PEZPTlQgIFNJWkU9MyBGQU1JTFk9IlNB TlNTRVJJRiIgRkFDRT0iQXJpYWwgTmFycm93IiBMQU5HPSIwIj48Qj5JbiBhIG1lc3NhZ2UgZGF0 ZWQgMy8xMS8wMSA3OjI3OjMxIFBNIEVhc3Rlcm4gU3RhbmRhcmQgVGltZSwgDQo8QlI+QS52YW5B cnVtQGNoZWxsby5ubCB3cml0ZXM6DQo8QlI+DQo8QlI+PC9GT05UPjxGT05UICBDT0xPUj0iIzAw MDAwMCIgU0laRT0yIEZBTUlMWT0iU0FOU1NFUklGIiBGQUNFPSJBcmlhbCIgTEFORz0iMCI+PC9C Pg0KPEJSPjwvRk9OVD48Rk9OVCAgQ09MT1I9IiMwMDAwZmYiIFNJWkU9MiBGQU1JTFk9IlNBTlNT RVJJRiIgRkFDRT0iQXJpYWwiIExBTkc9IjAiPjxCTE9DS1FVT1RFIFRZUEU9Q0lURSBzdHlsZT0i Qk9SREVSLUxFRlQ6ICMwMDAwZmYgMnB4IHNvbGlkOyBNQVJHSU4tTEVGVDogNXB4OyBNQVJHSU4t UklHSFQ6IDBweDsgUEFERElORy1MRUZUOiA1cHgiPkluIER1YmxpbiBJIHJlYWQgcGFydCBvZiB0 aGUgYm9vayBvbiB0aGUgaGlzdG9yeSBvZiB0aGUgbWFwLWNvbG91cmluZyANCjxCUj5wcm9ibGVt IGFuZCBob3cgaXQgd2FzIHNvbHZlZCwgd2hpY2ggd2FzIHJlYWxseSBpbnRlcmVzdGluZyB0byBy ZWFkIC0gaXQgDQo8QlI+d2FzIG9uZSBvZiB0aGUgZmlyc3QgcHJvb2ZzIGluIHdoaWNoIGNvbXB1 dGVycyBwbGF5ZWQgYSBncmVhdCBwYXJ0IGFuZCANCjxCUj5oZW5jZSBpdCB3YXMgYW5kIHN0aWxs IGlzIHZlcnkgY29udHJvdmVyc2lhbC4gPC9GT05UPjxGT05UICBDT0xPUj0iIzAwMDAwMCIgU0la RT0zIEZBTUlMWT0iU0FOU1NFUklGIiBGQUNFPSJBcmlhbCIgTEFORz0iMCI+PC9CTE9DS1FVT1RF Pg0KPEJSPjwvRk9OVD48Rk9OVCAgQ09MT1I9IiMwMDAwMDAiIFNJWkU9MyBGQU1JTFk9IlNBTlNT RVJJRiIgRkFDRT0iQXJpYWwgTmFycm93IiBMQU5HPSIwIj48Qj4NCjxCUj5BcndpbiwgDQo8QlI+ DQo8QlI+V2hhdCdzIHRoZSBib29rPyBUaGUgcmVhc29uIHRoZSBwcm9vZiB3YXMgY29udHJvdmVy c2lhbCBpcyB0aGF0IGl0IGlzbid0IA0KPEJSPmFjdHVhbGx5IGEgInByb29mIiBpbiBhbnkgbG9n aWNhbCBvciBtYXRoZW1hdGljYWwgc2Vuc2UuIEp1c3QgYSBicnV0ZSBmb3JjZSANCjxCUj5leGFt aW5pbmcgb2YgYWxsIGV4YW1wbGVzIHRoZSBjb21wdXRlciBjb3VsZCB0aGluayBvZiwgYW5kIG5v IHByb29mIChvciB3YXkgDQo8QlI+b2YgcHJvdmluZykgdGhhdCB0aGUgcHJvZ3JhbSB3YXMgYWN0 dWFsbHkgc3VmZmljaWVudCB0byB0ZXN0ICJldmVyeSIgcG9zc2libGUgDQo8QlI+ZXhhbXBsZS4g DQo8QlI+DQo8QlI+UGVyc29uYWxseSwgSSB0aGluayB0aGUgbWFwLWNvbG9yaW5nIHByb2JsZW0g aXMgYSBkZXNpZ24gcHJvYmxlbSwgbm90IGEgDQo8QlI+bWF0aGVtYXRpY2FsIHByb2JsZW0sIGFu ZCB0aGF0J3MgcHJlY2lzZWx5IHdoeSBwcm9ibGVtcyBhcm9zZSBpbiB0cnlpbmcgdG8gDQo8QlI+ Zm9ybXVsYXRlIGEgc29sdXRpb24gaW4gbWF0aGVtYXRpY2FsIHRlcm1zLiBPbmUgcXVlc3Rpb24g aXMgd2hldGhlciB0aGVyZSBhcmUgDQo8QlI+Y3JpdGVyaWEgZm9yIGlkZW50aWZ5aW5nIGEgbWF0 aGVtYXRpY2FsIHByb2JsZW0gYXMgb3Bwb3NlZCB0byBzb21lIG90aGVyIGtpbmQgDQo8QlI+b2Yg cHJvYmxlbS4gSWYgdGhlc2UgY3JpdGVyaWEgZXhpc3QsIEkgc3VyZSBkb24ndCBzZWUgd2hlcmUg dGhleSBhcmUsIGFuZCB0aGUgDQo8QlI+ZW52ZWxvcGUgY2FuJ3QgYmUgcHVzaGVkIHRvIGluY2x1 ZGUgYW55IHF1ZXN0aW9uIHdpdGggYSBudW1lcmljYWwgYW5zd2VyLiANCjxCUj5UaGVyZSdzIG5v IHByb3ZhYmxlIG1hdGhlbWF0aWNhbCBmb3JtdWxhLCBmb3IgZXhhbXBsZSwgdGhhdCBhbGxvd3Mg YW55b25lIHRvIA0KPEJSPmRldGVybWluZSB3aGF0IG51bWJlcnMgYXJlIHVzZWQgb24gdGhlIGxp Y2Vuc2UgcGxhdGUgZm9yIG15IGNhci4gQW5kIHRoZSANCjxCUj5xdWVzdGlvbiBpc24ndCBhY3R1 YWxseSBhIG1hdGhlbWF0aWNhbCBxdWVzdGlvbiwgZXZlbiB0aG91Z2ggdGhlIGFuc3dlciBjYW4g DQo8QlI+YmUgZXhwcmVzc2VkIGluIG51bWJlcnMuIE9uZSBjYW4gZ2V0IGFuIGFuc3dlciBieSBj aGVja2luZyB0aGUgbW90b3IgdmVoaWNsZSANCjxCUj5yZWNvcmRzLiBCdXQgbG9va2luZyB1cCBh IG51bWJlciBvbiBhIGxpc3QgaXNuJ3QgdGhlIHNhbWUgdGhpbmcgYXMgDQo8QlI+Y29uc3RydWN0 aW5nIGEgbWF0aGVtYXRpY2FsIHByb29mLi4udW5sZXNzIG1hdGhlbWF0aWNpYW5zIGFyZSB3aWxs aW5nIHRvIA0KPEJSPmJyb2FkZW4gdGhlaXIgc3RhbmRhcmQgb2Ygd2hhdCBjb25zdGl0dXRlcyBh IG1hdGhlbWF0aWNhbCBwcm9vZiBzbyB0aGF0IGl0IA0KPEJSPmluY2x1ZGVzIGFsbCB0aGUgInRy aXZpYWwiIHByb29mcyB0aGF0IHNlZW0gdG8gYmUgaWdub3JlZCBhdCBwcmVzZW50Lg0KPEJSPg0K PEJSPkkgdGhpbmsgQ2FudG9yIGRldmVsb3BlZCBzb21lIHByb29mIHRoYXQgdGhlcmUgY2FuJ3Qg YmUgYW55IGhpZ2hlc3QgcG9zc2libGUgDQo8QlI+bnVtYmVyIG9yIGFueSBlbmQgdG8gdGhlIG51 bWJlciBzZXJpZXMuLi53aGljaCB0ZW5kcyB0byB2YWxpZGF0ZSB0aGUgY29tbW9uIA0KPEJSPnNl bnNlIG9ic2VydmF0aW9uIHRoYXQgbm8gbWF0dGVyIGhvdyBsYXJnZSBhIG51bWJlciBpcywgb25l IGNhbiBhbHdheXMgYWRkIDEgDQo8QlI+dG8gaXQuIFNvIHdoeSBzaG91bGQgd2UgYmVsaWV2ZSBh IGNvbXB1dGVyIHRoYXQgZXJyb25lb3VzbHkgdGVsbHMgdXMgdGhhdCANCjxCUj50aGVyZSBhY3R1 YWxseSBpcyBhIGhpZ2hlc3QgcG9zc2libGUgbnVtYmVyLi4udGhpcyBiZWluZyB0aGUgaGlnaGVz dCBudW1iZXIgDQo8QlI+dGhhdCB0aGlzIHBhcnRpY3VsYXIgY29tcHV0ZXIgY2FuIGV4cHJlc3Mg Z2l2ZW4gaXRzIGxpbWl0YXRpb25zIG9mIG1lbW9yeSBhbmQgDQo8QlI+dGVjaG5vbG9neT8NCjxC Uj4NCjxCUj5JbiBhbnkgY2FzZSwgSSdkIGxpa2UgdG8gc2VlIHRoZSBhY3R1YWwgcHJvZ3JhbSBm b3Igc3VwcG9zZWRseSAicHJvdmluZyIgdGhlIA0KPEJSPmZvdXIgY29sb3IgdGhlb3JlbSwgd2hp Y2ggSSB0aGluayBjYW1lIGZyb20gVSBvZiBJbGxpbm9pcy4gV2FzIGl0IHJlcHJpbnRlZCANCjxC Uj5pbiB0aGUgYm9vayB5b3UgcmVhZD8gSXQncyBzdXBwb3NlZCB0byBiZSB0ZXJpYmJseSBsb25n LCByYXRoZXIgdGhhbiBhIA0KPEJSPnJlbGF0aXZlbHkgc2hvcnQgcHJvZ3JhbSB0aGF0J3MgdXNl ZCByZWN1cnNpdmVseS4gSSdkIGxpa2UgdG8gc2VlIHdoZXRoZXIgDQo8QlI+d2hhdCBtYWRlIGl0 IHNvIGxvbmcgaXMgYW4gYXR0ZW1wdCB0byBkZWZpbmUgImV2ZXJ5IHBvc3NpYmxlIiBzaXR1YXRp b24uICZuYnNwOw0KPEJSPg0KPEJSPlRoZXJlIHdhcyBhIHBlcmlvZCwgeW91IGtub3csIHdoZW4g YW4gYXR0ZW1wdCB3YXMgbWFkZSB0byBkZW1vbnN0cmF0ZSB0aGF0IA0KPEJSPmNvbXB1dGVycyBj YW4gZG8gYWxsIGtpbmRzIG9mIHRoaW5ncyB0aGV5IGFyZW4ndCBhY3R1YWxseSBjYXBhYmxlIG9m IGRvaW5nLiANCjxCUj5PbmUgZW5naW5lZXIgd2FzIGNsYWltaW5nIGEgY29tcHV0ZXIgY291bGQg bWFrZSBNb25kcmlhbiBwYWludGluZ3MsIGFuZCANCjxCUj5hbm90aGVyIHN0YXJ0ZWQgdGhhdCBz dHVwaWQgInRoZSBNb25hIExpc2EgaXMgTGVvbmFyZG8gaW4gZHJhZyIgc3R1ZmYuIEhlcmUsIA0K PEJSPnRoZSBhcmd1bWVudHMgd2VyZSBzZXQgZm9ydGggaW4gcmVsYXRpdmVseSBicmllZiBhcnRp Y2xlcy4gQW5kIHdoZW4gb25lIA0KPEJSPmZpbmlzaGVkIHJlYWRpbmcgdGhlIGFydGljbGVzLCBv bmUgcmVhbGl6ZWQgZWFjaCB3YXMgd3JpdHRlbiBieSBhIHBlcnNvbiB3aG8gDQo8QlI+ZGlkbid0 IGtub3cgYSB0aGluZyBhYm91dCBhcnQsIGFuZCB0aGVyZWZvcmUgZGlkbid0IGtub3cgaG93IHRv IGludGVycHJldCB0aGUgDQo8QlI+ZGF0YS4NCjxCUj4NCjxCUj5JbiB0aGUgNC1jb2xvciB0aGVv cmVtLCB0b28sIGl0IHNlZW1zIHRvIG1lIGZyb20gd2hhdCBJJ3ZlIHJlYWQgdGhhdCB0aGUgDQo8 QlI+cHJvZ3JhbW1lcnMgc2tpcHBlZCB0b28gbWFueSBzdGVwcy4gU3RhcnRpbmcgYXQgc3F1YXJl IG9uZSwgdGhlIGZpcnN0IGpvYiBpcyANCjxCUj50byBwcm9ncmFtIGEgY29tcHV0ZXIgdG8gY29u c3RydWN0IG1hdGhlbWF0aWNhbCBwcm9vZnMuIFVudGlsIHRoYXQncyBiZWVuIA0KPEJSPmFjY29t cGxpc2hlZCwgYSBjb21wdXRlciBpc24ndCBhYmxlIHRvIGNvbnN0cnVjdCBhIG1hdGhlbWF0aWNh bCBwcm9vZiBvZiANCjxCUj5hbnl0aGluZy4gQW5kIHRoaXMgb2YgY291cnNlIGlzIHRoZSBib3Jk ZXJsaW5lIHF1ZXN0aW9uIHRoYXQgSSBob3BlIGlzIGJlaW5nIA0KPEJSPmNvbnNpZGVyZWQgaW4g QUkuIFdoYXQncyB0aGUgbGltaXQgdG8gd2hhdCBhIGNvbXB1dGVyIGNhbiBkbz8gQW5kIHdoYXQg DQo8QlI+cHJvYmxlbXMgY2FuIG9ubHkgYmUgc29sdmVkIGJ5IGEgc2VudGllbnQgYmVpbmc/DQo8 QlI+DQo8QlI+QWxsIHRoYXQgdG8tZG8gYWJvdXQgY29tcHV0ZXJzIHBsYXlpbmcgY2hlc3MgaXMg ZmFyIGZyb20gcGVyc3Vhc2l2ZSwgYmVjYXVzZSANCjxCUj5jaGVzcyBoYXMgYSBmaW5pdGUgbnVt YmVyIG9mIHBvc3NpYmxlIG1vdmVzLiAmbmJzcDtXaGF0IGFib3V0IHByb2dyYW1taW5nIGEgDQo8 QlI+Y29tcHV0ZXIgdG8gd3JpdGUgYSByZWNpcGUgYm9vaywgd2l0aCBzb21lIGFzc3VyYW5jZSB0 aGF0IHRoZSByZWNlaXBlcyB3aWxsIA0KPEJSPmJlIHN1cGVyaW9yIHRvIHRob3NlIGEgaHVtYW4g YmVpbmcgbWlnaHQgZGV2ZWxvcD8gJm5ic3A7SGVyZSwgaXQncyBhIHRvdWdoZXIgDQo8QlI+cHJv YmxlbSwgYmVjYXVzZSBtb3JlIGlzIGludm9sdmVkIHRoYW4gc2h1ZmZsaW5nIG51bWJlcnMsIHdo aWNoIGlzIGFsbCANCjxCUj5jb21wdXRlcnMgY2FuIGRvLiBCdXQsIGFzIGFib3ZlLCBJIHRoaW5r IHRoZSBtYWluIHByb2JsZW0gd2l0aCBhbnkgDQo8QlI+Y29tcHV0ZXJpemVkICJtYXRoZW1hdGlj YWwgcHJvb2YiIG9mIHRoZSBmb3VyLWNvbG9yIHRoZW9yZW0gaXMgdGhhdCBvbmUgY2FuJ3QgDQo8 QlI+c2tpcCB0aGUgbmVjZXNzYXJ5IHN0ZXAgb2YgZGV2ZWxvcGluZyBhIHByb2dyYW0gY2FwYWJs ZSBvZiBjb25zdHJ1Y3RpbmcgDQo8QlI+bWF0aGVtYXRpY2FsIHByb29mcy4gDQo8QlI+DQo8QlI+ cGF0DQo8QlI+DQo8QlI+DQo8QlI+PC9CPjwvRk9OVD48L0hUTUw+DQoNCg== --0__=Lo2ie8JCvFyKTEo9MdGo69gDqCO5GtVIFv0w67il0qMKPs8f5wNe3wmI--