 ## TSE@PO.MISSOURI.EDU

#### View:

 Message: [ First | Previous | Next | Last ] By Topic: [ First | Previous | Next | Last ] By Author: [ First | Previous | Next | Last ] Font: Monospaced Font  LISTSERV Archives  TSE Home  TSE March 2001

Subject: RE: OFF TOPIC - Map coloring

From: Date: Mon, 12 Mar 2001 20:15:08 +0100

Content-Type: text/plain

Parts/Attachments:  text/plain (662 lines)

Arwin,

What's the=20   book?

=
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.

The reason the proof = was=20   controversial is that it isn't
actually a "proof" in any logical = or=20   mathematical sense. Just a brute force
examining of all examples = the=20   computer could think of, and no proof (or way
of proving) that the = program=20   was actually sufficient to test "every" possible=20
example.

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.

Personally, I = think the=20   map-coloring problem is a design problem, not a
mathematical = problem, and=20   that's precisely why problems arose in trying to
formulate a = solution in=20   mathematical terms. One question is whether there are
criteria for =   identifying a mathematical problem as opposed to some other kind =
of=20   problem.
If these criteria = exist, I sure=20   don't see where they are, and the
envelope can't be pushed to = include any=20   question with a numerical answer.

=
Don't=20 you know that even the answer to the Question of Life is 42? ;-) (I just = love=20 Douglas Adams)
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.

There's no = provable=20   mathematical formula, for example, that allows anyone to
determine = what=20   numbers are used on the license plate for my car. And the
question = isn't=20   actually a mathematical question, even though the answer can
be = expressed=20   in numbers. One can get an answer by checking the motor vehicle =
records.=20   But looking up a number on a list isn't the same thing as =
constructing a=20   mathematical proof...unless mathematicians are willing to
broaden = their=20   standard of what constitutes a mathematical proof so that it =
includes all=20   the "trivial" proofs that seem to be ignored at=20   present.

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.

I think Cantor developed = some proof that=20   there can't be any highest possible
number or any end to the = number=20   series...which tends to validate the common
sense observation that = no=20   matter how large a number is, one can always add 1
to it. So why = should we=20   believe a computer that erroneously tells us that
there actually = is a=20   highest possible number...this being the highest number
that this=20   particular computer can express given its limitations of memory and=20
technology?

=
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

In any case, I'd like to see the actual = program=20 for supposedly "proving" the
four color theorem, which I think came = from U=20 of Illinois. Was it reprinted
in the book you read? It's supposed to = be=20 teribbly long, rather than a
relatively short program that's used=20 recursively. I'd like to see whether
what made it so long is an = attempt to=20 define "every possible" situation.

&nbs= p;
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.

There was a period, = you know,=20 when an attempt was made to demonstrate that
computers can do all = kinds of=20 things they aren't actually capable of doing.
One engineer was = claiming a=20 computer could make Mondrian paintings, and
another started that = stupid "the=20 Mona Lisa is Leonardo in drag" stuff. Here,
the arguments were set = forth in=20 relatively brief articles. And when one
finished reading the = articles, one=20 realized each was written by a person who
didn't know a thing about = art, and=20 therefore didn't know how to interpret the
data.

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

In=20 the 4-color theorem, too, it seems to me from what I've read that the=20
programmers skipped too many steps. Starting at square one, the = first job is=20
to program a computer to construct mathematical proofs. Until that's = been=20
accomplished, a computer isn't able to construct a mathematical = proof of=20
anything. And this of course is the borderline question that I hope = is being=20
considered in AI. What's the limit to what a computer can do? And = what=20
problems can only be solved by a sentient = being?

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.

All that to-do about = computers=20 playing chess is far from persuasive, because
chess has a finite = number of=20 possible moves.  What about programming a
computer to write a = recipe=20 book, with some assurance that the receipes will
be superior to = those a=20 human being might develop?  Here, it's a tougher
problem, = because more=20 is involved than shuffling numbers, which is all
computers can=20 do.

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.

But, as above, I think = the main=20 problem with any
computerized "mathematical proof" of the four-color = theorem=20 is that one can't
skip the necessary step of developing a program = capable of=20 constructing
mathematical proofs.

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.

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?

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

Arwin

------=_NextPart_000_0012_01C0AB31.22437F90--

#### Search Archives  Log In  Get Password  Search Archives  Subscribe or Unsubscribe