%\documentclass[11pt]{article}
%\usepackage{a4}\oddsidemargin 6pt\textwidth 431pt\pagestyle{plain}
\documentstyle[11pt]{article}
\def\qed{{\sf QED}}\def\mizar{{\sf Mizar}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%
\title{                          What Can \qed\ Offer to Mathematics?\\[1ex]
\large                           \qed\ Workshop II, Warsaw, July 20--22, 1995}

\author{                         Manfred Kerber\thanks
{                                Fachbereich Informatik, Universit\"at des
 Saarlandes,
                                 Im Stadtwald 15, D-66041 Saarbr\"ucken,
 Germany,
                                 e-mail: {\tt kerber@cs.uni-sb.de}, Tel.:
 (+49)681-302-4628.}}
\date{
        }
\begin{document}\maketitle
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%
\section{                           Correctness
                }

The main argument why \qed\ can be of great practical use is the ongoing
striving for correctness in mathematics at a level as high as possible: a system
like \qed\ is the answer of our time to that striving.  That this correctness
problem is not sufficiently solved in traditional mathematics can be seen in the
history of false theorems and false proofs.\vspace{1ex}

\noindent{\bf False theorems:} The perhaps best studied example of a theorem
 that had to
be corrected again and again is Euler's polyhedron theorem. Imre
Lakatos\footnote{see: Imre Lakatos. {\em Proofs and Refutations}. Cambridge
  University Press, 1976.} has described the cycle of stating the theorem,
proving it, and finding counterexamples, then going into the next loop with a
refined version of the theorem. How can it be possible that there are
counterexamples to a proved theorem? This can be due to inaccurate definitions,
hidden assumptions, or invalid arguments. The main problem in the case of
Euler's
polyhedron theorem has been what to consider as a polyhedron. A system like
\qed, however, would not accept any inaccurate definitions, hidden assumptions,
or invalid arguments, but it forces a human user to be precise.\vspace{1ex}

\noindent{\bf False proofs:} While the problem of false theorems is much more
grave than that of false proofs, false proofs, which can be patched, occur much
more often. This problem arises since mathematical proofs are normally not given
on a formal logical level, but on an intuitive level where the ideas how to
build a proof are conveyed rather than the proofs itself. On such a level it is
possible that a proof is not understandable or that certain non-trivial gaps may
occur (e.g.~in the proof of Fermat's Last Theorem), for which it is not clear
whether they can be closed or not.\vspace{1ex}

\qed\ can support the author, the reviewer, and the user of a theorem against
false theorems as well as against false proofs. For each theorem must exist a
machine-checked proof.


\section{                           Proof Presentation
                }

Proving mathematical theorems is a social process. The verification of
mathematical arguments is a key activity in mathematics and hence very sensitive
for the development of mathematics. Therefore it is not a good idea to try to
replace this process by checking proofs in \qed. On the contrary, \qed\ should
be considered as a supplement to the traditional process of proof checking and
supporting this process.  In particular \qed\ should support different levels of
the proof display (such as the logic level, assertional level, expert level with
a user model, interactive proof display, or even multi-media facilities).

\section{                           Information Retrieval
                }

While correctness and proof presentation may not be the main gains
mathematicians can draw from \qed, they may be very interested in using a large
data base of definitions and theorems, when it is well-organized and easy to
use. A large data base of mathematical facts in \qed\ can easily provide useful
information like the interdependence of certain axioms, definitions and
theorem, which is hard to obtain without computer support.

\section{                           Future Prospects
                }

In order to come up with a system that finds a broad distribution, \qed\
eventually has to enable a human user to develop a machine-checked proof at
least as easily as to do that on paper. Therefore it is necessary to provide
strong support in the proof search in more areas. In order to do that standard
automated theorem proving techniques as well as more high-level oriented
approaches like proof planning and analogy should be used.

But even when this goal is reached a lot of additional functionality can be
integrated in \qed, for instance support for some standard procedure of
mathematics, like the approach of changing the definitions in order to get the
right theorem.

\section{Discussion}
In the discussion the following points were made:
\begin{itemize}
\item Correctness may be too weak an argument for mathematicians when confronted
  with the \qed-approach, since at first a lot of basic work has to be done
  before they can really start. Furthermore errors in papers are normally not
  too important. Therefore \qed\ has to do a lot of preliminary work. In \mizar,
  for instance, thirty master theses were written. This led not only to a
  profound amount of formal mathematical knowledge, but had also the interesting
  side effect that the relationship between a teacher and a student changed a
  lot: the teacher does not force the student to be precise, but the system does
  and the teacher has the role of assisting the student. In order to increase
  the acceptance of \qed, it would be ideal to expose students to formal proving
  already in an early stage of their academic training.

\item It would be fine to have a collection of well-documented examples for
  false theorems and false proofs.

\item A main practical argument for mathematicians to use \qed\ could be the
  speed of publications. If the article is formally written in \qed, cumbersome
  proof reading can be done mechanically and the referees can concentrate on the
  relevance of the paper rather than on the correctness.
\end{itemize}

\end{document}