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