Re: Turing Machines and Physical Computation

From: Stephen Harris (cyberguard1048-usenet_at_yahoo.com)
Date: 11/24/04 

Date: Wed, 24 Nov 2004 03:29:24 GMT

<tchow@lsa.umich.edu> wrote in message
news:41a3ef28$0$576$b45e6eb0@senator-bedfellow.mit.edu...
> In article <ZDPod.21741$zx1.19672@newssvr13.news.prodigy.com>,
> Stephen Harris <cyberguard1048-usenet@yahoo.com> wrote:
> [Re: distrust of computer-assisted proofs]
>>I thought there were cases of theorems considered to be proven that
>>were later discovered not to be proven, because the computer was
>>programmed in error? So how do you know for sure.
>
> There are also cases of theorems considered to be proven that were later
> discovered to have erroneous proofs, where no computer was involved, and
> the only error involved was human error.
>

Yes, this is true.

> The attitude of most mathematicians nowadays is that every proof has some
> risk of being wrong. The computer-assisted part of a proof, if properly
> managed, tends to be *less* likely to have errors than the "human" part.
> (Not that everyone properly manages their computer-assisted proofs.
> Then again, not everyone properly manages their non-computer-assisted
> proofs either.)
>

I read back issues of the FOM mailing list because it is free and
fascinating.
Your contributions have been noted. My second favor author is Joe Shipman
who I notice expresses his reservations mildly, "we can not have the same
type of certainty" whereas I used the cruder "distrust". "There is alway
some distrust of computer aided proofs."

http://www.cs.nyu.edu/pipermail/fom/1998-August/002076.html Joe Shipman:
"In the absence of rigorous proofs of the correctness of computer systems
(including chip design, programming language, compiler, and operating
system),
we can not have the same type of certainty about the correctness of a
computer-aided proof as we can of a humanly surveyable proof.

But we can attain "moral" certainty if we follow Nicely's recipe with
sufficient thoroughness (I would demand more than two verifications in which
all the components of the system were independent for an important result
like 4CT or the Kepler conjecture).

[SH: Shipman supports your point in this paragraph.]
"Conventional" proofs are not always more certain than this. Three
illustrations:
1) Smale's paper on "Problems for the 21st Century" in the Spring 1998
Mathematical Intelligencer (which I recommended to FOM a few months ago)
mentions in passing a shockingly large number of incorrect "theorems" which
were originally accepted and took years to be recognized as not really
proved
2) Hsiang's 1990 "proof" of the Kepler conjecture, a consensus against which
was obtained only several years later (the paper still has not been
withdrawn)
3) The classification of finite simple groups is said to be several thousand
pages long and I do not believe any single mathematician has carefully
checked
the entire thing; thus no one can have the confidence that this theorem is
true that they can have about a proof they have personally checked, everyone
can have only the confidence attainable from accepting the authority of
other
mathematicians, which is less. (I'm not even sure every piece of the proof
of
the Classification has been validated by several referees yet -- does anyone
know if this has yet occurred?) For example, I have personally verified
proofs of the Prime Number Theorem and Godel's Incompleteness Theorem; I
depend on the authority of other mathematicians for my belief in Wiles's
("Fermat's Last") Theorem and Friedman's latest independence results, though
I
look forward to one day personally verifying them.

---------------------------------------------------------------------
tchow wrote:
> The dissatisfaction with computer-assisted proofs stems mostly from the
> feeling that they don't give a lot of insight.

SH: Harvey Friedman, my favorite FOM author agrees with you.

http://www.cs.nyu.edu/pipermail/fom/1998-September/002210.html
Harvey Friedman "But the deep foundational question is, not whether
it is true, but what does it mean?"
> --

Again, I appreciate the correction about the 1928 date and challenge.
It certainly makes more sense that way!

Regards,
Stephen

Relevant Pages

  • Re: Turing Machines and Physical Computation
    ... My second favor author is Joe Shipman ... type of certainty" whereas I used the cruder "distrust". ... "In the absence of rigorous proofs of the correctness of computer systems ... depend on the authority of other mathematicians for my belief in Wiles's ...
    (sci.math)
  • Re: Cantors Theory sucks
    ... >>> truth of its axiom systems is not presumed except as a convenient ... > ultimately mere verification of the correctness of if-then statements ... > Pure math only deals with correctness, ... > Pure mathematicians are sort of like the tool makers for those applied ...
    (sci.math)
  • Re: Multiple-Choice Exams in Math? Good Idea?
    ...  I am curious as to what most mathematicians think of multiple choice exams in mathematics. ... correctness of the answer. ... The other style is when students have to "justify their answers", ... zero for a wrong answer if this is due only to a minor miscalculation. ...
    (sci.math)
  • Re: Test Driven Development
    ... Mathematicians who actually study proofs tell us that a "proof of ... correctness" is impossible inside a computer. ... Those mathematicians ... flexible software faster. ...
    (comp.object)
  • Re: Cold, hard facts defy the doomsayers
    ... While we are speaking of certainties, what degree of certainty (I've asked ... expert climatologists are always very good mathematicians. ... who says I'm lacking in math skills? ...
    (sci.geo.geology)