From owner-qed Mon Nov 14 03:14:34 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id DAA24900 for qed-out; Mon, 14 Nov 1994 03:12:30 -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 DAA24894 for <qed@mcs.anl.gov>; Mon, 14 Nov 1994 03:12:25 -0600
Received: from delphi.com by delphi.com (PMDF V4.3-9 #7804)
 id <01HJGFJCPVV4A0X7UE@delphi.com>; Mon, 14 Nov 1994 04:12:22 -0500 (EST)
Date: Mon, 14 Nov 1994 04:12:22 -0500 (EST)
From: Lyle Burkhead <LYBRHED@delphi.com>
Subject: The Fermat-Wiles Theorem
To: qed@mcs.anl.gov
Message-id: <01HJGFJCPVV6A0X7UE@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


>if you could use the QED system in order to verify a proof as 
>complex and convoluted as Wiles' proof, you'd demonstrate to all 
>mathematicians [the] enormous usefulness of such a system. 

Why?  What would that tell the mathematicians that they don't 
already know?  

If you found a mistake in the proof after everyone accepted it, that 
would cause consternation.  Imagine what the New York Times 
would do with that story!  But if you spend 20 years and millions 
of dollars to verify something that is already known to be true, in 
what sense are you "demonstrating the enormous usefulness of 
such a system"?  

Lyle