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.