From owner-qed Fri Nov 18 03:04:19 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id DAA18133 for qed-out; Fri, 18 Nov 1994 03:03:13 -0600
Received: from bos1a.delphi.com (SYSTEM@bos1a.delphi.com [192.80.63.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id DAA18128 for ; Fri, 18 Nov 1994 03:03:08 -0600
Received: from delphi.com by delphi.com (PMDF V4.3-9 #7804)
id <01HJM0E706NK9FME92@delphi.com>; Fri, 18 Nov 1994 04:03:06 -0500 (EST)
Date: Fri, 18 Nov 1994 04:03:06 -0500 (EST)
From: Lyle Burkhead
Subject: The Fermat-Wiles Theorem
To: qed@mcs.anl.gov
Message-id: <01HJM0E70GAQ9FME92@delphi.com>
X-VMS-To: INTERNET"qed@mcs.anl.gov"
MIME-version: 1.0
Content-type: TEXT/PLAIN; CHARSET=US-ASCII
Content-transfer-encoding: 7BIT
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
John Staples writes,
>This is what *assurance* is all about - recognising the value
>of having checked, even if the outcome is boringly satisfactory.
>The aircraft industry and many other industries put huge
>dollar values on assurance.
Airplanes crash. Proofs don't. Last year I asked if anyone could
give an example of a theorem which was published in a textbook
or reputable journal, accepted by the mathematicians who read
it and used by them in further work, and then found to be
false. No one ever came up with such an example.
It is an illusion to think that QED is needed to "verify" a proof,
such as the Wiles proof, that has received the intense scrutiny of
many competent mathematicians.
Programs, of course, do crash. QED could certainly be useful in
computer science and engineering, where the mathematics is
tedious, complex, and not at all intuitive. Victor Yodiaken made
this point very well in his message of July 5, 1993. If QED
provides assurance that computer systems (and other complex
systems) will perform according to their specifications, industry
will certainly put a huge dollar value on such assurance.
However, QED was originally conceived as a project comprising
"all of mathematics." If it is going to degenerate into a tool for
engineers, it is a waste of time (from a scientific standpoint).
What can QED offer pure mathematicians? This question may
have an answer, but the answer is not "verification."
Lyle