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 ; 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
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