FOM: mathematical certainty

[Anatoly Vorobey]

You, Stephen Cook, were spotted writing this on Fri, Nov 20, 1998 at 02:23:42PM -0500:
> My point of view is that "mathematically certain" means that there exists a formal
> proof in an appropriate formal system; say ZFC.  The authors of both theorems
> are trying to convince us that such a proof exists.   I don't know which (group
> of) author(s) has done the more convincing job, but the necessary use of computers
> to check the four-color theorem proof does NOT make it less convincing.  

It would be fascinating to hear more responses on this, obviously foundational,
issue. Rota's point is that mathematicians in general *do* feel very 
strongly that the necessary use of computers to check the 4CT makes the claim
of its validity less convincing. 

> Both
> computers and mathematicians can make mistakes:  to decide which argument is more
> convincing one has to consider who checked each one and how it was checked.

It seems to me that you're aiming for some kind of (however limited) equality
of mathematicians and computers when validity of a theorem is to be
considered - please correct me if I'm wrong! However, even the very statement
"both computers and mathematicians can make mistakes" is very much
"human-centered": a computer never makes a mistake from "its own" point of view,
it just sits there and works. Mistakes "happen" when the results it produces
don't match our, human, expectations.

You're saying

> one has to consider who checked each one and how it was checked.

But how is the considering done, according to which principles? 

Presumably, running one program on one computer obviously isn't enough. 
Even running one program on many different computers isn't enough. Is running
two independent programs on many computers the same as letting two
mathematicians check a theorem independently? How many indepedent programs
would you need to write and run before you can believe in 4CT with the
same certainty as you believe, e.g. that each vector space has a basis?

It's certainly *conceivable* that the methods used to prove FLT gradually
become so widely known and understood that in 100 years FLT would be intuitively 
perceived by mathematicians to be as obvious as the Hahn-Banach theorem.
Could the same level of certainty be reached by piling more and more
independent programs verifying 4CT?

> In the case of the 4CT, part of the checking should involve writing an inpendent
> computer program and running it on a different computer.

That (if my memory doesn't betray me) has been done. Does it allow one to
consider the matter as settled?

-- 
Anatoly Vorobey,
mellon at pobox.com http://pobox.com/~mellon/
"Angels can fly because they take themselves lightly" - G.K.Chesterton