From owner-qed Mon Nov 21 06:59:41 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id GAA17421 for qed-out; Mon, 21 Nov 1994 06:57:54 -0600
Received: from wonder (toor@wonder.irst.it [192.70.136.8]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id GAA17415 for <qed@mcs.anl.gov>; Mon, 21 Nov 1994 06:57:34 -0600
Received: from goedel by wonder with SMTP id AA25512
  (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>); Mon, 21 Nov 1994 14:02:02 +0100
Received: by goedel id AA06426
  (5.65c/IDA-1.4.4); Mon, 21 Nov 1994 13:57:03 +0100
From: Manfred Kerber <kerber@irst.it>
Message-Id: <199411211257.AA06426@goedel>
Subject: Re: Errors in Mathematics
To: LYBRHED@delphi.com (Lyle Burkhead)
Date: Mon, 21 Nov 1994 13:57:02 +0100 (MET)
Cc: qed@mcs.anl.gov
In-Reply-To: <01HJQ1HO7NH89GY4ZQ@delphi.com> from "Lyle Burkhead" at Nov 21, 94 01:18:04 am
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
Content-Length: 2398      
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Lyle Burkhead wrote

> About false theorems:  we still don't have any.  The examples 
> given were all correct results with incorrect or incomplete proofs.  

Perhaps the most famous at least the best studied example of a ``false
theorem'' is Euler's polyhedron theorem that states the relationship
between the numbers of vertices, edges, and surfaces of a polyhedron
(e+s=v+2). In ``Proofs and Refutations'', Imre Lakatos describes the
fascinating history of the cycle:

1) a false theorem is stated
   (false because the definition of a polyhedron is incorrect),
2) a false proof is constructed,
3) a counter-example is detected and the whole cycle restarts by patching
   the definition.

The whole process of correcting this false theorem took over 100 years
if I remember right.

Using computers for proof checking cannot provide an *absolute*
guarantee of correctness, but a very improved level. In any reasonable
implementation of QED the fuzzy definitions of a polyhedron would have
been rejected and in particular it would not have been possible to
derive the theorem from the faulty definition.

Of more significance for mathematics have been false theorems like the
convergence of SUM_n=1^infinity 1/n. This has lead to a new foundation
of the calculus by Weierstrass in giving precise definitions of up to
that time fuzzy notions of convergence, limits, and so on. Systems
like QED can be seen as the answer of our time and of our technology
to the older question how can we guarantee correctness to a degree as
high as possible. In my opinion, such systems should not replace the
human refereeing process but supplement it.

+-------------------------------------------------------------------------+
| Manfred Kerber,                                                         |
| Omega-MKRP Project, Fachbereich Informatik, Universit"at des Saarlandes |
| D-66041 Saarbr"ucken, Germany, kerber@cs.uni-sb.de                      |
|                                                                         |
| currently at:                                                           |
| Mechanized Reasoning Group, IRST                                        |
| (Istituto per la Ricerca Scientifica e Tecnologica),                    |
| I-38050 Povo (Trento), Italy, kerber@irst.it                            |
+-------------------------------------------------------------------------+