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