From owner-qed Mon Nov 21 00:19:24 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id AAA15498 for qed-out; Mon, 21 Nov 1994 00:18:15 -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 AAA15493 for <qed@mcs.anl.gov>; Mon, 21 Nov 1994 00:18:09 -0600
Received: from delphi.com by delphi.com (PMDF V4.3-9 #7804)
 id <01HJQ1HO7NH69GY4ZQ@delphi.com>; Mon, 21 Nov 1994 01:18:04 -0500 (EST)
Date: Mon, 21 Nov 1994 01:18:04 -0500 (EST)
From: Lyle Burkhead <LYBRHED@delphi.com>
Subject: Errors in Mathematics
To: qed@mcs.anl.gov
Message-id: <01HJQ1HO7NH89GY4ZQ@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


Let me withdraw the expression "waste of time" and rephrase 
my point as follows:  QED was originally conceived as a project 
comprising "all of mathematics."  If it turns out to be of use only 
to engineers, it will not have achieved its intended purpose.  

Richard Schroeppel writes:  

  >I believe the published mathematics literature contains a 
  >significant number of errors.  Most are at the typo level, 
  >but there are some number of missing terms, missing 
  >hypotheses, and important wrong words. Long calculations, 
  >and tables, frequently have errors.  Many journals have a 
  >section for Errata & Corrections.  If QED could fix these prior 
  >to publication, we would be better off.

Agreed.  Whenever a mathematical paper is submitted to a 
journal (in machine-readable form), it could be run through QED 
and checked before publication.  QED would work like a compiler.  
It would attempt to translate the paper into low-level logic and 
generate error messages if it ran into difficulties.  This would 
certainly be an excellent way to eliminate errors.  We all know 
what a joy it is to read a program listing with hundreds of 
obscure error messages due to typos and other minor mistakes, 
and I'm sure mathematicians would be eternally grateful for this 
service... ;-)

Seriously, this provides an answer to the question:  Who are the 
customers of QED?  The customers are journal editors.    

About false theorems:  we still don't have any.  The examples 
given were all correct results with incorrect or incomplete proofs.  
The Four Color Theorem, the Hard Lefschetz Theorem, and Dehn's 
Lemma all turned out to be true.  Not only that, the erroneous 
proofs were noticed by human mathematicians, not by automated 
reasoning systems.  I have never encountered a false theorem 
that was used as the foundation for other theorems, with 
disastrous results.  And I don't think anybody else has, either.  
There are many imperfections in the mathematical literature, 
and some incomplete proofs, but I don't think there are any 
substantive errors that affect the integrity of mathematics.  

Lyle