From owner-qed Mon Nov 21 03:58:58 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id DAA16552 for qed-out; Mon, 21 Nov 1994 03:56:33 -0600 Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id DAA16547 for ; Mon, 21 Nov 1994 03:56:28 -0600 Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id DAA00551; Mon, 21 Nov 1994 03:00:02 -0700 Message-Id: <199411211000.DAA00551@chelm.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Mon, 21 Nov 1994 03:00:01 -0700 In-Reply-To: Lyle Burkhead "Errors in Mathematics" (Nov 21, 1:18am) reply_to: yodaiken@chelm.nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: Lyle Burkhead , qed@mcs.anl.gov Subject: Re: Errors in Mathematics Sender: owner-qed@mcs.anl.gov Precedence: bulk On Nov 21, 1:18am, Lyle Burkhead wrote: Subject: Errors in Mathematics > >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. 1) Many of us are interested in the verification of computer systems. Thus, the types of mathematical proofs we primarily wish to verify are rather applied and mundane ones. 2) There are areas of pure mathematics, notably in combinatorics, where one encounters complexities quite similar to those which make proofs of computer system correctness so difficult and tedious. 3) If one cannot build theorem provers that prove useful to computer engineers, it seems quite likely that one cannot solve the harder problem of theorem provers for pure mathematicians. 4) I also find it very doubtful that mathematics suffers from a problem of incorrect theorems that will only be rooted out by QED. Leslie Lamport, who seems to be the main publicist of the contrary view, has, in my ever so humble opinion, failed to understand the difference between computer programs that will not compile with a simple error and proofs that serve the purpose of communication even if they contain errors.