This is a multi-part message in MIME format. ------=_NextPart_000_0012_01C0AB31.22437F90 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: 7bit Arwin, What's the book? I think it was the Fritz book; I only remember that it was very accessible and that it was published around 1998, so it must be. 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. Well, much has been said about this already. I'd like to stress that once you can write a computer program to do something, you can usually also always prove that. Whether or not the proof is elegant is a wholly different matter, but a computer program is nothing but a series of logical and computational statements and those can be fully described by logic and meta-logic. Again, as has been said elsewhere, once it has been established that a solution can be found, but that verification requires an amount of calculation that is beyond human capacity, you're almost there as a mathematician. What has basically been done is that the proof has been split into hundreds of different problems that each need a significant amount of calculation to be able to verify them. It is not unlikely that at some point each of these hundreds of problems will be proven more elegantly, but if you can prove them by the brute force of just testing every possible sub-case this suffices. You then only need to prove that the calculation done by the computer is correct, and as I said, this is (at least theoretically) always possible and has been proven possible in this case as well, I think, although it could also be that the theory has simply been verified by using it to write another program which produced the same results. If they made the same mistake twice then you never know until someone shows that the proof's not in the pudding - as happened before with the first time the four colours made it from conjecture to theorem. 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. Don't you know that even the answer to the Question of Life is 42? ;-) (I just love Douglas Adams) But seriously, once a mathematician sets himself the goal to prove using mathematics that a map can always be coloured in using only four colours, then it has become a mathematical problem. If you look at a map and want to colour it in using red, blue, yellow and orange, it has become a design problem. It's that simple - all just a matter of perspective. 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 could construct a formula which makes your licence plate the result of factors like date, place of registry, available numbers, dealer, build-year, or whatever. I could use that to predict the numbers for your licence plate. That has nothing to do with proof. Once a mathematician sets himself the task of proving that my formula works for any given case, it has become a mathematical proof. Of course, if I thought mathematical proofs were really important for understanding the world, I would have studied math and not English lit. 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 the terms you're discussing numbers and computers now, a computer will indicate when its calculations supercede its capabilities by giving an 'overflow' message. Calculations which produce an infinitely large number, like dividing 1/0, also sometimes produce this message. However, a computer program is not necessarily as limited and its capabilities for number crunching can be largely extended. I wrote routines that use strings to process numbers, for instance, which means that you can work with numbers that fill a whole encyclopedia or larger. Even then, however, you can verify that even these greatly increased capabilities have been surpassed by the problem at hand. 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. What made it so long was that there were programs written for 1200 sub problems. If it could have been a short program, then I promise you that the proof would been found sooner and would have been elegant. 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. This perhaps explains your scepticism but has very little to do with the role of computers in proving anything. As a programmer I know that a computer program is every bit as stupid or clever as its programmer. 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? But this, of course, is a wholly different matter. The computer didn't construct the proof - it just did the boring work of veryfying the proof. There will, one day, perhaps come a point where the computer will provide a much more elegant program which accomplishes the same task much more efficiently, but don't hold your breath. 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. There seems to be a persistent prejudice that because the word computer means count stuff the computer can only shift numbers. I could say very unpleasant things about yourself if I based myself purely on what your braincells can do, particularly in terms of reliability. 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. Well, let it then be clear that this is a complete misunderstanding of the problem. There are two parts to mathematical problems. One is devising a theory, and the other is providing the proof. The proof can be theoretical, or the proof can be practical. Usually once the practical proof has been achieved, this is stronger proof than theoretical proof, because to be one-hundred percent certain of a theoretical proof you just have to be sure that the theory will correctly predict any given situation that lies within its domain, and the least doubtful way of doing so is to test it with every possible situation within its domain. That is not to say that it will be great to develop a program that can devise mathematical proofs as well as verify them, but I predict this will also raise another problem. At some point there won't be any human left who is capable of understanding any of it, and we'll end up in the situation so humorously described by Douglas Adams (man makes computer to solve question "what's the meaning of life"; computer cannot solve problem but proposed to build a computer that can build a computer which can solve the question. Three generations and a lifetime of calculation later the computer prompts an answer: "42". "42?" says the people, "42? How can this be? This is nonsense ... ". "Well," says the computer, " are you certain you understand the question? Which brings me to another point. What if we managed to write a computerprogram which can write stories which are even funnier than those by Douglas Adams. Would we be delighted or frightened out of our wits? (I know what I am, but I'm also pretty certain it would be possible to do - not as hard as writing a computer program which can write computer programs to solve any given problem, although in theory this could be more efficient). Arwin ------=_NextPart_000_0012_01C0AB31.22437F90 Content-Type: text/html; charset="US-ASCII" Content-Transfer-Encoding: quoted-printable <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> <HTML><HEAD> <META content=3D"text/html; charset=3Dus-ascii" = http-equiv=3DContent-Type> <META content=3D"MSHTML 5.00.2920.0" name=3DGENERATOR></HEAD> <BODY> <BLOCKQUOTE=20 style=3D"BORDER-LEFT: #0000ff 2px solid; MARGIN-LEFT: 5px; PADDING-LEFT: = 5px"> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><BR><STRONG>Arwin, <BR><BR>What's the=20 book? </STRONG><SPAN class=3D271273018-12032001><FONT = color=3D#0000ff=20 face=3DArial size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 = class=3D271273018-12032001></SPAN></FONT></FONT> </DIV></BLOCKQUOTE>= <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001><EM> </EM>I think it was the Fritz book; = I only=20 remember that it was very accessible and that it was published around = 1998, so=20 it must be. </SPAN></FONT></DIV> <BLOCKQUOTE=20 style=3D"BORDER-LEFT: #0000ff 2px solid; MARGIN-LEFT: 5px; PADDING-LEFT: = 5px"> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><STRONG>The reason the proof = was=20 controversial is that it isn't <BR>actually a "proof" in any logical = or=20 mathematical sense. Just a brute force <BR>examining of all examples = the=20 computer could think of, and no proof (or way <BR>of proving) that the = program=20 was actually sufficient to test "every" possible=20 <BR>example. <BR></STRONG><SPAN class=3D271273018-12032001><FONT=20 color=3D#0000ff face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV></BLOCKQUOTE> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>Well, much has been said about this already. = I'd like=20 to stress that once you can write a computer program to do something, = you can=20 usually also always prove that. Whether or not the proof is elegant is a = wholly=20 different matter, but a computer program is nothing but a series of = logical and=20 computational statements and those can be fully described by logic and=20 meta-logic. Again, as has been said elsewhere, once it has been = established that=20 a solution can be found, but that verification requires an amount of = calculation=20 that is beyond human capacity, you're almost there as a mathematician. = What has=20 basically been done is that the proof has been split into hundreds of = different=20 problems that each need a significant amount of calculation to be able = to verify=20 them. It is not unlikely that at some point each of these hundreds of = problems=20 will be proven more elegantly, but if you can prove them by the brute = force of=20 just testing every possible sub-case this suffices. You then only need = to prove=20 that the calculation done by the computer is correct, and as I said, = this is (at=20 least theoretically) always possible and has been proven possible in = this case=20 as well, I think, although it could also be that the theory has simply = been=20 verified by using it to write another program which produced the same = results.=20 If they made the same mistake twice then you never know until someone = shows that=20 the proof's not in the pudding - as happened before with the first time = the four=20 colours made it from conjecture to theorem.</SPAN></FONT></DIV> <BLOCKQUOTE=20 style=3D"BORDER-LEFT: #0000ff 2px solid; MARGIN-LEFT: 5px; PADDING-LEFT: = 5px"> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><BR><STRONG>Personally, I = think the=20 map-coloring problem is a design problem, not a <BR>mathematical = problem, and=20 that's precisely why problems arose in trying to <BR>formulate a = solution in=20 mathematical terms. One question is whether there are <BR>criteria for = identifying a mathematical problem as opposed to some other kind = <BR>of=20 problem. </STRONG></FONT></FONT><FONT = face=3Darial,helvetica><FONT=20 color=3D#000000 face=3D"Arial Narrow" lang=3D0 size=3D3 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><STRONG>If these criteria = exist, I sure=20 don't see where they are, and the <BR>envelope can't be pushed to = include any=20 question with a numerical answer. </STRONG><SPAN=20 class=3D271273018-12032001><FONT color=3D#0000ff face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 = class=3D271273018-12032001></SPAN></FONT></FONT> </DIV></BLOCKQUOTE>= <DIV><FONT color=3D#0000ff face=3DArial size=3D2><SPAN = class=3D271273018-12032001>Don't=20 you know that even the answer to the Question of Life is 42? ;-) (I just = love=20 Douglas Adams) </SPAN></FONT></DIV> <DIV><FONT color=3D#0000ff face=3DArial size=3D2><SPAN = class=3D271273018-12032001>But=20 seriously, once a mathematician sets himself the goal to prove using = mathematics=20 that a map can always be coloured in using only four colours, then it = has become=20 a mathematical problem. If you look at a map and want to colour it in = using red,=20 blue, yellow and orange, it has become a design problem. It's that = simple - all=20 just a matter of perspective. </SPAN></FONT></DIV> <BLOCKQUOTE=20 style=3D"BORDER-LEFT: #0000ff 2px solid; MARGIN-LEFT: 5px; PADDING-LEFT: = 5px"> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><BR><STRONG>There's no = provable=20 mathematical formula, for example, that allows anyone to <BR>determine = what=20 numbers are used on the license plate for my car. And the <BR>question = isn't=20 actually a mathematical question, even though the answer can <BR>be = expressed=20 in numbers. One can get an answer by checking the motor vehicle = <BR>records.=20 But looking up a number on a list isn't the same thing as = <BR>constructing a=20 mathematical proof...unless mathematicians are willing to <BR>broaden = their=20 standard of what constitutes a mathematical proof so that it = <BR>includes all=20 the "trivial" proofs that seem to be ignored at=20 present. <BR></STRONG><SPAN class=3D271273018-12032001><FONT = color=3D#0000ff=20 face=3DArial = size=3D2> </FONT></SPAN></FONT></FONT></DIV></BLOCKQUOTE> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>I could construct a formula which makes your = licence=20 plate the result of factors like date, place of registry, available = numbers,=20 dealer, build-year, or whatever. I could use that to predict the numbers = for=20 your licence plate. That has nothing to do with proof. Once a = mathematician sets=20 himself the task of proving that my formula works for any given case, it = has=20 become a mathematical proof. Of course, if I thought mathematical proofs = were=20 really important for understanding the world, I would have studied math = and not=20 English lit. </SPAN></FONT></DIV> <BLOCKQUOTE=20 style=3D"BORDER-LEFT: #0000ff 2px solid; MARGIN-LEFT: 5px; PADDING-LEFT: = 5px"> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><BR><STRONG>I think Cantor developed = some proof that=20 there can't be any highest possible <BR>number or any end to the = number=20 series...which tends to validate the common <BR>sense observation that = no=20 matter how large a number is, one can always add 1 <BR>to it. So why = should we=20 believe a computer that erroneously tells us that <BR>there actually = is a=20 highest possible number...this being the highest number <BR>that this=20 particular computer can express given its limitations of memory and=20 <BR>technology? </STRONG><SPAN class=3D271273018-12032001><FONT=20 color=3D#0000ff face=3DArial = size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 = class=3D271273018-12032001></SPAN></FONT></FONT> </DIV></BLOCKQUOTE>= <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN class=3D271273018-12032001><FONT = color=3D#0000ff=20 face=3DArial size=3D2>In the terms you're discussing numbers and = computers now, a=20 computer will indicate when its calculations supercede its capabilities = by=20 giving an 'overflow' message. Calculations which produce an infinitely = large=20 number, like dividing 1/0, also sometimes produce this message. However, = a=20 computer program is not necessarily as limited and its capabilities for = number=20 crunching can be largely extended. I wrote routines that use strings to = process=20 numbers, for instance, which means that you can work with numbers that = fill a=20 whole encyclopedia or larger. Even then, however, you can verify that = even these=20 greatly increased capabilities have been surpassed by the problem at = hand.=20 </FONT></SPAN><BR><BR><STRONG>In any case, I'd like to see the actual = program=20 for supposedly "proving" the <BR>four color theorem, which I think came = from U=20 of Illinois. Was it reprinted <BR>in the book you read? It's supposed to = be=20 teribbly long, rather than a <BR>relatively short program that's used=20 recursively. I'd like to see whether <BR>what made it so long is an = attempt to=20 define "every possible" situation. </STRONG><FONT = size=3D2><FONT=20 color=3D#0000ff><FONT face=3DArial><SPAN=20 class=3D271273018-12032001> </SPAN></FONT></FONT></FONT></FONT></FON= T><FONT=20 face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial Narrow" = lang=3D0 size=3D3=20 FAMILY=3D"SANSSERIF"><FONT size=3D2><FONT color=3D#0000ff><FONT = face=3DArial><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT></FONT></FONT></FONT></DI= V> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><FONT size=3D2><FONT color=3D#0000ff><FONT = face=3DArial><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT></FONT></FONT></FONT>&nbs= p;</DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><FONT size=3D2><FONT color=3D#0000ff><FONT = face=3DArial><SPAN class=3D271273018-12032001>What made it so long was = that there=20 were programs written for 1200 sub problems. If it could have been a = short=20 program, then I promise you that the proof would been found sooner and = would=20 have been elegant. </SPAN></FONT></FONT></FONT></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><BR><STRONG>There was a period, = you know,=20 when an attempt was made to demonstrate that <BR>computers can do all = kinds of=20 things they aren't actually capable of doing. <BR>One engineer was = claiming a=20 computer could make Mondrian paintings, and <BR>another started that = stupid "the=20 Mona Lisa is Leonardo in drag" stuff. Here, <BR>the arguments were set = forth in=20 relatively brief articles. And when one <BR>finished reading the = articles, one=20 realized each was written by a person who <BR>didn't know a thing about = art, and=20 therefore didn't know how to interpret the <BR>data. </STRONG><SPAN = class=3D271273018-12032001><FONT color=3D#0000ff face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>This perhaps explains your scepticism but has = very=20 little to do with the role of computers in proving anything. As a = programmer I=20 know that a computer program is every bit as stupid or clever as its = programmer.=20 </SPAN></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN = class=3D271273018-12032001> </SPAN><STRONG>In=20 the 4-color theorem, too, it seems to me from what I've read that the=20 <BR>programmers skipped too many steps. Starting at square one, the = first job is=20 <BR>to program a computer to construct mathematical proofs. Until that's = been=20 <BR>accomplished, a computer isn't able to construct a mathematical = proof of=20 <BR>anything. And this of course is the borderline question that I hope = is being=20 <BR>considered in AI. What's the limit to what a computer can do? And = what=20 <BR>problems can only be solved by a sentient = being? <BR></STRONG><SPAN=20 class=3D271273018-12032001><FONT color=3D#0000ff face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>But this, of course, is a wholly different = matter. The=20 computer didn't construct the proof - it just did the boring work of = veryfying=20 the proof. There will, one day, perhaps come a point where the computer = will=20 provide a much more elegant program which accomplishes the same task = much more=20 efficiently, but don't hold your breath. </SPAN></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><BR><STRONG>All that to-do about = computers=20 playing chess is far from persuasive, because <BR>chess has a finite = number of=20 possible moves. What about programming a <BR>computer to write a = recipe=20 book, with some assurance that the receipes will <BR>be superior to = those a=20 human being might develop? Here, it's a tougher <BR>problem, = because more=20 is involved than shuffling numbers, which is all <BR>computers can=20 do. </STRONG><SPAN class=3D271273018-12032001><FONT color=3D#0000ff = face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT color=3D#0000ff face=3DArial size=3D2><SPAN = class=3D271273018-12032001>There=20 seems to be a persistent prejudice that because the word computer means = count=20 stuff the computer can only shift numbers. I could say very unpleasant = things=20 about yourself if I based myself purely on what your braincells can do,=20 particularly in terms of reliability. </SPAN></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT></FONT> </DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001> </SPAN><STRONG>But, as above, I think = the main=20 problem with any <BR>computerized "mathematical proof" of the four-color = theorem=20 is that one can't <BR>skip the necessary step of developing a program = capable of=20 constructing <BR>mathematical proofs. <BR></STRONG><SPAN=20 class=3D271273018-12032001><FONT color=3D#0000ff face=3DArial=20 size=3D2> </FONT></SPAN></FONT></FONT></DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>Well, let it then be clear that this is a = complete=20 misunderstanding of the problem. There are two parts to mathematical = problems.=20 One is devising a theory, and the other is providing the proof. The = proof can be=20 theoretical, or the proof can be practical. Usually once the practical = proof has=20 been achieved, this is stronger proof than theoretical proof, because to = be=20 one-hundred percent certain of a theoretical proof you just have to be = sure that=20 the theory will correctly predict any given situation that lies within = its=20 domain, and the least doubtful way of doing so is to test it with every = possible=20 situation within its domain. </SPAN></FONT></DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT> </DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>That is not to say that it will be great to = develop a=20 program that can devise mathematical proofs as well as verify them, but = I=20 predict this will also raise another problem. At some point there won't = be any=20 human left who is capable of understanding any of it, and we'll end up = in the=20 situation so humorously described by Douglas Adams (man makes computer = to solve=20 question "what's the meaning of life"; computer cannot solve problem but = proposed to build a computer that can build a computer which can solve = the=20 question. Three generations and a lifetime of calculation later the = computer=20 prompts an answer: "42". "42?" says the people, "42? How can this be? = This is=20 nonsense ... ". "Well," says the computer, " are you certain you = understand the=20 question? </SPAN></FONT></DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001></SPAN></FONT> </DIV> <DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 = FAMILY=3D"SANSSERIF"><SPAN=20 class=3D271273018-12032001>Which brings me to another point. What if we = managed to=20 write a computerprogram which can write stories which are even funnier = than=20 those by Douglas Adams. Would we be delighted or frightened out of our = wits? (I=20 know what I am, but I'm also pretty certain it would be possible to do - = not as=20 hard as writing a computer program which can write computer programs to = solve=20 any given problem, although in theory this could be more efficient).=20 </SPAN></FONT></DIV> <DIV><FONT face=3Darial,helvetica><FONT color=3D#000000 face=3D"Arial = Narrow" lang=3D0=20 size=3D3 FAMILY=3D"SANSSERIF"><SPAN = class=3D271273018-12032001> </SPAN><BR><FONT=20 size=3D2><FONT color=3D#0000ff><FONT face=3DArial><SPAN=20 class=3D271273018-12032001>Arwin</SPAN><BR><BR></FONT></FONT></FONT></DIV= ></FONT></FONT></BODY></HTML> ------=_NextPart_000_0012_01C0AB31.22437F90--