This is a multipart message in MIME format.
=_NextPart_000_0012_01C0AB31.22437F90
ContentType: text/plain;
charset="USASCII"
ContentTransferEncoding: 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
metalogic. 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 subcase
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 mapcoloring 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, buildyear,
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 4color 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 todo 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 fourcolor 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
onehundred 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
ContentType: text/html;
charset="USASCII"
ContentTransferEncoding: quotedprintable
<!DOCTYPE HTML PUBLIC "//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META content=3D"text/html; charset=3Dusascii" =
httpequiv=3DContentType>
<META content=3D"MSHTML 5.00.2920.0" name=3DGENERATOR></HEAD>
<BODY>
<BLOCKQUOTE=20
style=3D"BORDERLEFT: #0000ff 2px solid; MARGINLEFT: 5px; PADDINGLEFT: =
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=3D27127301812032001><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=3D27127301812032001></SPAN></FONT></FONT> </DIV></BLOCKQUOTE>=
<DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 =
FAMILY=3D"SANSSERIF"><SPAN=20
class=3D27127301812032001><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"BORDERLEFT: #0000ff 2px solid; MARGINLEFT: 5px; PADDINGLEFT: =
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=3D27127301812032001></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=3D27127301812032001> </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=3D27127301812032001><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=3D27127301812032001>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
metalogic. 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 subcase 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"BORDERLEFT: #0000ff 2px solid; MARGINLEFT: 5px; PADDINGLEFT: =
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=3D27127301812032001> </SPAN><BR><STRONG>Personally, I =
think the=20
mapcoloring 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=3D27127301812032001> </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=3D27127301812032001><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=3D27127301812032001></SPAN></FONT></FONT> </DIV></BLOCKQUOTE>=
<DIV><FONT color=3D#0000ff face=3DArial size=3D2><SPAN =
class=3D27127301812032001>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=3D27127301812032001>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"BORDERLEFT: #0000ff 2px solid; MARGINLEFT: 5px; PADDINGLEFT: =
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=3D27127301812032001> </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=3D27127301812032001><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=3D27127301812032001>I could construct a formula which makes your =
licence=20
plate the result of factors like date, place of registry, available =
numbers,=20
dealer, buildyear, 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"BORDERLEFT: #0000ff 2px solid; MARGINLEFT: 5px; PADDINGLEFT: =
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=3D27127301812032001><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=3D27127301812032001></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=3D27127301812032001><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=3D27127301812032001> </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=3D27127301812032001></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=3D27127301812032001></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=3D27127301812032001>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=3D27127301812032001> </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=3D27127301812032001><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=3D27127301812032001></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=3D27127301812032001></SPAN></FONT></FONT> </DIV>
<DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 =
FAMILY=3D"SANSSERIF"><SPAN=20
class=3D27127301812032001>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=3D27127301812032001></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=3D27127301812032001> </SPAN><STRONG>In=20
the 4color 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=3D27127301812032001><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=3D27127301812032001>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=3D27127301812032001> </SPAN><BR><STRONG>All that todo 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=3D27127301812032001><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=3D27127301812032001></SPAN></FONT></FONT> </DIV>
<DIV><FONT color=3D#0000ff face=3DArial size=3D2><SPAN =
class=3D27127301812032001>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=3D27127301812032001></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=3D27127301812032001> </SPAN><STRONG>But, as above, I think =
the main=20
problem with any <BR>computerized "mathematical proof" of the fourcolor =
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=3D27127301812032001><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=3D27127301812032001>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
onehundred 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=3D27127301812032001></SPAN></FONT> </DIV>
<DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 =
FAMILY=3D"SANSSERIF"><SPAN=20
class=3D27127301812032001>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=3D27127301812032001></SPAN></FONT> </DIV>
<DIV><FONT color=3D#0000ff face=3DArial lang=3D0 size=3D2 =
FAMILY=3D"SANSSERIF"><SPAN=20
class=3D27127301812032001>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=3D27127301812032001> </SPAN><BR><FONT=20
size=3D2><FONT color=3D#0000ff><FONT face=3DArial><SPAN=20
class=3D27127301812032001>Arwin</SPAN><BR><BR></FONT></FONT></FONT></DIV=
></FONT></FONT></BODY></HTML>
=_NextPart_000_0012_01C0AB31.22437F90
