\documentclass[runningheads]{llncs}
\usepackage[all]{xypic}
\usepackage{amssymb,url}
\raggedbottom
\def\mizerror#1{\strut\rlap{\hspace\hsize\ \texttt{*#1}}}
\def\xverb#1{\underbar{\tt{#1}}}
\def\xsemi{\xverb{;}}
\def\Z{{\mathbb Z}}
\begin{document}
\title{Formal Proof Sketches}
\author{Freek Wiedijk}
\institute{Department of Computer Science, University of Nijmegen\\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\maketitle
\begin{abstract}
Formalized mathematics
%(proofs written in sufficient
%detail that a computer program can check the correctness)
currently does not look much like informal mathematics.
%even when using a declarative systems like Mizar or Isabelle/Isar.
%
Also, formalizing mathematics
currently seems far too much work to be worth the time of the
working mathematician.
%(to get the mathematical community interested in formalization
%one would like to have an approach to formalization where one
%can in a natural way leave `gaps' in the reasoning.)
%
To address both of these problems we introduce the notion of a
\emph{formal proof sketch}.
This is a proof representation that is in between
a fully checkable formal proof
and a statement without any proof at all.
Although a formal proof sketch is too high level to be checkable
by computer, it has a precise notion of correctness (hence the
adjective \emph{formal}).
We will show through examples that formal proof sketches
can closely mimic already existing mathematical proofs.
Therefore, although a formal proof sketch
contains gaps in the reasoning from a formal point of view
(which is why we call it a \emph{sketch}), a mathematician probably would
call such a text just a `proof'.
\end{abstract}
\section{Introduction}
\subsection{Problem}\label{section:problem}
This paper is about formalization of mathematics:
the encoding of mathematics in a formal language
in sufficient detail that a computer program can verify
the correctness.
The systems that are currently most suitable for this
are Coq, NuPRL/MetaPRL, Mizar, Isabelle/Isar, HOL and PVS.
Of these systems Mizar and Isabelle/Isar are \emph{declarative},
which means that the input language of the system is designed to
be similar to the language of the informal proofs that one finds in
mathematical papers and textbooks.
Two main applications of formalized mathematics are:
\begin{enumerate}
\item \emph{representation},
and from this \emph{presentation}, of the mathematics
\item verification of the mathematical \emph{correctness} of the mathematics
\end{enumerate}
However, if one looks at the current state of the art in formal mathematics,
then both seem to have difficulties:
\begin{itemize}
\item
A mathematical formalization currently almost always is
a big tar file on an ftp server.
Inside such a tar file one finds a number of `proof script' files,
which mostly resemble program source code.
Even with the declarative systems Mizar and Isabelle/Isar
these files are
not readable as ordinary mathematical text.
At best one can read them like one might study a computer program.
%to find out how it works.
%
This means that the files of a formalization by themselves are useless
to communicate the mathematics that is in them.
For this reason several people have developed tools that produce natural
language versions of formalized proofs.
However, we have never seen a convincing demo of such a system
where we were able to follow a non-trivial proof by reading the
generated text.
The output of such a tool generally is an order of magnitude
larger than the proof scripts that were the input,
and also it is rather monotone, as it is automatically generated by
a computer program.
%%
%Most of these systems use \emph{subproof folding} to deal with
%this size problem,
%but then one tends to get `lost in the subproof tree' when navigating
%the subproof hierarchy of such a proof.
%
For these reasons, we consider current formalizations not well suited
for the communication of mathematics:
the proof script files are unreadable,
while the generated natural language presentation is generally too
verbose and too monotone
%and often too badly structured,
to keep the reader's attention
needed to understand the mathematics.
In practice,
to find out what is in a formalization
people almost exclusively look at the statements of the lemmas
and ignore the proofs (which generally are not in the files
that they look at anyway).
They only use the proofs for \emph{proof engineering}, like
modifying a copy of a proof to prove a similar lemma,
or changing a proof to make it check faster or extract to a better
program.
\item
Formalization of mathematics is a very labor-intensive activity.
A rough estimate of the amount of work needed for the formalization
of mathematics is that with the current state of the art
it takes about one work-week (five days
from nine to five) to formalize one page from an undergraduate
mathematics textbook.
Eventually, we would like the mathematicians to start using our systems
for routine formalization of mathematics.
However, currently it will be unrealistic to
expect working mathematicians to go to the trouble of doing full
formalizations.
Even with a proper mathematical library (which currently is not available
for any of the existing systems) the cost of doing a full formalization
is prohibitive in comparison to the benefit.
At the TYPES workshop of 2002 in Nijmegen, Peter Aczel claimed
that in order to get mathematicians involved with the
formalization of mathematics,
technology is needed for
\emph{reasoning with gaps}, where one can leave out the details
of a formalization that one considers to be obvious or
well-known, and one only needs
to formalize the interesting parts.
This vision is the focus of this paper.
\end{itemize}
\subsection{Approach}
We will define the notion of a \emph{formal proof sketch}
for the declarative proof language of the Mizar system \cite{muz:93,wie:99:1}.
A formal proof sketch is an incomplete Mizar text that only has one
kind of error -- that justifications do not
necessarily justify the steps,
the famous \texttt{*4} error of the Mizar system --
such that it can be completed into a correct
Mizar text by adding steps, and references between the steps, to the proofs.
%See Section \ref{section:fps} below for a
%definition of the notion of formal proof sketch.
Although this paper uses Mizar as the declarative proof
language,
the notion of formal proof sketch makes sense for any
declarative language.
For instance one can have formal proof sketches for Markus Wenzel's
Isar language for the Isabelle system \cite{wen:02},
or for the proof language of Don Syme's Declare system \cite{sym:99}.
\subsection{Contribution}
`An unfinished Mizar article that has only \texttt{*4} errors left in it'
is a well-known concept to every Mizar user.
However, we think it is new to consider such a text to be
more important than just being an intermediate stage during
formalization.
In fact, we would like to claim
that that kind of text might be \emph{more} interesting
and useful than a completed Mizar formalization.
Also, it is new to use this kind as text as
a \emph{presentation} of the contents of a finished formalization.
New also is the observation that many informal mathematical
proofs from the literature
can be mimicked closely by formal proof sketches.
(This is a primarily an observation on the syntax of the Mizar language.)
See for examples Sections \ref{section:sqrt2} and \ref{section:examples}
below.
%
Finally it is new to consider the incomplete
justifications of a formal proof sketch to be
natural targets for automated theorem proving,
as discussed in Section \ref{section:atp}.
As far as we know no system exists yet that uses the same declarative
language both on the formal proof sketch level and on the formalization
level. %, in the integrated way outlined in Section \ref{section:cycle}.
The main contribution of this paper is the proposal of building such a system.
\subsection{Outline}
In Section \ref{section:sqrt2} we give a detailed example of
a formal proof sketch.
In Sections \ref{section:fps} and \ref{section:cycle} we discuss the notion of formal proof sketch.
In Sections \ref{section:genlang} and \ref{section:lamport} we compare
formal proof sketches with other approaches to proof presentation.
In Section \ref{section:atp} we point out the relation between
formal proof sketches and automated theorem proving.
In Section \ref{section:examples} we present two more
examples.
\section{An Example: Four Versions of the Irrationality of $\sqrt{2}$}\label{section:sqrt2}
On pages 39 and 40 of the fourth edition of Hardy and Wright's {\em An Introduction to the Theory of Numbers\/}
\cite{har:wri:60},
we find the following proof:
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
{\sc Theorem 43 (Pythagoras' theorem).} {\em $\sqrt{2}$ is irrational.}
\medskip\noindent
The traditional proof ascribed to Pythagoras runs
as follows. If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{(4.3.1)}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$. Hence $a^2$ is even, and there%-
fore $a$ is even. If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$. \hfill$\Box$%
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
%This is the kind of prose that one finds in informal mathematical texts,
%and it is very different from the kind of text that one finds in a
%proof assistant.
If we mimic this text in Mizar syntax, it turns out that
we get surprisingly close:
\pagebreak
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}\label{example}
{\sc theorem} Th43:$\,$ {\it $\mathop{\mbox{\rm sqrt}} 2$ is irrational\/} $\,$:: {\sc Pythagoras' theorem}
\medskip\noindent
{\sc proof}$\,$ assume $\mathop{\mbox{\rm sqrt}} 2$
is rational; consider $a,b$ such that
$$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$
and $a,b$ are\_relative\_prime; $a\mathbin{\hat{}}2$ is even;
then $a$ is even; consider $c$ such that $a = 2\mathbin{*}c$; $4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$; then $2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$; $b$ is
even; thus contradiction; \hfill{\sc end};%
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
This is \emph{almost} a correct Mizar text,
because the reasoning is too high level for the system to
know why the steps in this proof are allowed
(to turn it into a correct Mizar formalization one needs to add
intermediate steps and labels, as shown below).
%See below for this completed version.
%
However,
this text is \emph{syntactically} completely correct according to the Mizar grammar.
To stress this, we repeat it in conventional Mizar layout:
%(apart from the layout, this
%is the same as the previous text):
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}\footnotesize
\begin{tabular}{lcl}
\verb|theorem Th43: sqrt 2 is irrational| &$\hspace{13.2em}$& \\
\verb|proof| && \\
\verb| assume sqrt 2 is rational;| && \\
\verb| consider a,b such that| && \\
\verb|4_3_1: a^2 = 2*b^2 and| && \\
\verb| a,b are_relative_prime;| && \rlap{\quad$\mathord{\leftarrow}1$} \\
\verb| a^2 is even;| && \rlap{\quad$\mathord{\leftarrow}2$} \\
\verb| a is even;| && \rlap{\quad$\mathord{\leftarrow}3$} \\
\verb| consider c such that a = 2*c;| && \rlap{\quad$\mathord{\leftarrow}4$} \\
\verb| 4*c^2 = 2*b^2;| && \rlap{\quad$\mathord{\leftarrow}5$} \\
\verb| 2*c^2 = b^2;| && \rlap{\quad$\mathord{\leftarrow}6$} \\
\verb| b is even;| && \rlap{\quad$\mathord{\leftarrow}7$} \\
\verb| thus contradiction;| && \rlap{\quad$\mathord{\leftarrow}8$} \\
\verb|end;|
\end{tabular}
\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
If one runs this through the Mizar system, one
gets eight times the error
`\emph{this inference is not accepted}'
(as indicated by the arrows in the right margin).
The following text is a completed Mizar formalization of the same proof,
where the errors have been eliminated.
The parts that correspond to the previous text have been underlined:
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}\footnotesize
\begin{flushleft}
\xverb{theorem Th43: sqrt 2 is irrational}\\
\xverb{proof}\\
\verb| |\xverb{assume sqrt 2 is rational;}\\
\verb| then |\xverb{consider a,b such that}\\
\verb|A1: b <> 0 and|\\
\verb|A2: sqrt 2 = a/b and|\\
\verb|A3: |\xverb{a,b are\char`_relative\char`_prime}\verb| by Def1;|\\
\verb|A4: b^2 <> 0 by A1,SQUARE_1:73;|\\
\verb| 2 = (a/b)^2 by A2,SQUARE_1:def 4|\\
\verb| .= a^2/b^2 by SQUARE_1:69;|\\
\verb| then|\\
\xverb{4\char`_3\char`_1: a\^{}2 = 2*b\^{}2}\verb| by A4,XCMPLX_1:88|\xsemi\\
\verb| |\xverb{a\^{}2 is even}\verb| by 4_3_1,ABIAN:def 1|\xsemi\\
\verb| |\verb|then|\\
\verb|A5: |\xverb{a is even}\verb| by PYTHTRIP:2|\xsemi\\
\verb| then |\xverb{consider c such that}\\
\verb|A6: |\xverb{a = 2*c}\verb| by ABIAN:def 1|\xsemi\\
\verb|A7: |\xverb{4*c\^{}2 =}\verb| (2*2)*c^2|\\
\verb| .= 2^2*c^2 by SQUARE_1:def 3|\\
\verb| .= |\xverb{2*b\^{}2}\verb| by A6,4_3_1,SQUARE_1:68|\xsemi\\
\verb| 2*(2*c^2) = (2*2)*c^2 by XCMPLX_1:4|\\
\verb| .= 2*b^2 by A7;|\\
\verb| then |\xverb{2*c\^{}2 = b\^{}2}\verb| by XCMPLX_1:5|\xsemi\\
\verb| then b^2 is even by ABIAN:def 1;|\\
\verb| then |\xverb{b is even}\verb| by PYTHTRIP:2|\xsemi\\
\verb| then 2 divides a & 2 divides b by A5,Def2;|\\
\verb| then|\\
\verb|A8: 2 divides a gcd b by INT_2:33;|\\
\verb| a gcd b = 1 by A3,INT_2:def 4;|\\
\verb| |\xverb{hence contradiction}\verb| by A8,INT_2:17|\xsemi\\
\xverb{end;}
\end{flushleft}
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
Note that this formalization does not much resemble the Hardy and Wright
proof anymore but looks like the kind of `code' that is customary
in proof assistants.
\medskip
\noindent
This example shows the three kinds of proof texts that we will
consider in this paper:
\begin{itemize}
\item
the first text fragment is an \emph{informal English proof}
\item
the second and third are a \emph{formal proof sketch}
(in two different layouts)
\item
the fourth is a \emph{full formalization}
\end{itemize}
We imagine a prover interface in which all these variant texts
are present next to each other,
connected by hyperlinks.
Note that the informal English proof and the formal proof sketch are very similar.
Also note that the formal proof sketch and the full formalization are both written
in the same formal language.
Finally note that the formal proof sketch occurs as a `skeleton' in the
text of the full formalization.
This paper proposes to take these formal proof sketches seriously.
%We will define the notion of formal proof sketch in the next
%section.
We claim that a formal proof sketch can be used to precisely
communicate mathematics (although the computer cannot check the
correctness, a human can, cf.~the proposition on page \pageref{proposition}).
We also claim that a formal proof sketch is the best way to present
a formalization, as a `road map' to the full text of the formalization.
For two more examples of an informal English proof together with
a formal proof sketch version, see Section \ref{section:examples}
at the end of this paper.
%\begin{quote}
%\begin{verbatim}
% redefine attr x is rational means
%:Def1: ex a,b st b <> 0 & x = a/b & a,b are_relative_prime;
%\end{verbatim}
%\end{quote}
%\begin{quote}
%\begin{verbatim}
% redefine attr a is even means
%:Def2: 2 divides a;
%\end{verbatim}
%\end{quote}
\section{Formal Proof Sketches}\label{section:fps}
We now give the informal definition of a formal proof sketch.
This definition can be made rigorous but we will not do that
here.
\medskip
\noindent
\textbf{Definition. }%
A \emph{formal proof sketch} is a text in the syntax of a declarative proof
language that was obtained from a full formalization in that language
by removing some proof steps and references between proof steps.
The only errors (according to the definition of the proof language)
in such a stripped formalization
should be \emph{justification errors}:
the errors that say that
a step is not sufficiently justified by the references to previous steps.
%\begin{center}
%\begin{tabular}{rcl}
%statement &$\;$=$\;$& \emph{formula} $[\,$\textbf{proof} $\{$step \textbf{;}$\}$ $[\,$cases$\,]$ \textbf{end}$\,]$ \\
%\noalign{\medskip}
%step &=& statement
% \\
% &$|$& \textbf{assume} \emph{formula}
% \\
% &$|$& \textbf{let} \emph{variable} $\{$\textbf{,} \emph{variable}$\}$ \\
% &$|$& \textbf{thus} \emph{formula} \\
% &$|$& \textbf{consider} \emph{variable} $\{$\textbf{,} \emph{variable}$\}$
% \textbf{such} \textbf{that} \emph{formula} \\
% &$|$& \textbf{take} \emph{term} $\{$\textbf{,} \emph{term}$\}$ \\
%\noalign{\medskip}
%cases &=& \textbf{per} \textbf{cases} \textbf{;}
% $\big\{$\textbf{suppose} \emph{formula}\textbf{;} $\{$step \textbf{;}$\}\big\}\hspace{-3em}$
%\end{tabular}
%\end{center}
\medskip
\noindent
Some people might object to the name `formal proof \emph{sketch}',
claiming that these formal proof sketches are designed to closely follow
the informal proofs of mathematics, and that mathematicians
consider those to be \emph{proofs}, and not sketches.
However, we would like to take the formalizer's point of view that
formal proof sketches leave parts of the mathematics implicit,
and that therefore we can use the word `sketch'.
If we specialize the notion of a formal proof sketch
to the Mizar proof language,
we have the following \emph{formal proof sketch grammar}:
\begin{center}
\begin{tabular}{rcl}
statement &$\;$=$\;$& proposition {justification} \\
&$|$& {$[\,$\emph{label} \textbf{:}$\,]$} \emph{term} \textbf{=} \emph{term} {justification} \\
&& \quad $\{$\textbf{.=} \emph{term} {justification}$\}$ \\
\noalign{\medskip}
proposition &=& {$[\,$\emph{label} \textbf{:}$\,]$} formula \\
\noalign{\medskip}
formula &=& \emph{formula} \\ &$|$& \textbf{thesis} \\
\noalign{\medskip}
justification &=& {$[\,$\textbf{by} \emph{label} $\{$\textbf{,} \emph{label}$\}\,]$} \\
&{$|$}& \textbf{proof} $\{$step \textbf{;}$\}$ $[\,$cases$\,]$ \textbf{end} \\
\noalign{\medskip}
step &=& {$[\,$\textbf{then}$\,]$} statement \\
&$|$& \textbf{assume} proposition \\
&$|$& \textbf{let} \emph{variable} $\{$\textbf{,} \emph{variable}$\}$ \\
&$|$& {$(\,$}\textbf{thus} {$|$ \textbf{hence}$\,)$} statement \\
&$|$& {$[\,$\textbf{then}$\,]$} \textbf{consider} \emph{variable} $\{$\textbf{,} \emph{variable}$\}$ \\
&& \quad \textbf{such} \textbf{that} proposition {justification} \\
&$|$& \textbf{take} \emph{term} $\{$\textbf{,} \emph{term}$\}$ \\
&$|$& \textbf{set} \emph{variable} \textbf{=} \emph{term}
\\
\noalign{\medskip}
cases &=& \textbf{per} \textbf{cases} {justification} \textbf{;} \\
&& \quad $\big\{$\textbf{suppose} proposition \textbf{;} $\{$step \textbf{;}$\}\big\}\hspace{-3em}$
\end{tabular}
\end{center}
\noindent
%(In this grammar \emph{label}, \emph{variable},
%\emph{term} and \emph{formula} are taken to be primitive.)
%
Note that we do not propose our own proof language here.
We use the Mizar system to experiment
with formal proof sketches
and therefore we do not want to depart from the Mizar syntax.
%
Also note that this grammar is small.
Often people seem to have the impression that Mizar has a
complex syntax, but the proof
part of the language is really not much larger than this.
We can graphically represent the process of removing steps and references
from a formalization to obtain a formal proof sketch:
$$\label{graph}
\xymatrix@=1.5em{
& *+[F]{a}\ar[d] & & &&
{a}\ar[d] & & &&
{a} & \\
& *+[F]{b}\ar[dl]\ar[d]\ar[dr] & & &&
{b}\ar@/_1pc/[ddd]\ar[dr] & & &&
{b} & \\
{c}\ar[d] & {d}\ar[d] & *+[F]{e}\ar[dl]\ar[ddd] &&
& & {e}\ar[ddl]\ar@/^1pc/[dddd] & &&
& {e} \\
{f}\ar[dr] & {g}\ar[d] & & &&
& & &&
& \\
& *+[F]{h}\ar[d] & & &&
{h}\ar[ddr] & & &&
{h} & \\
& {i}\ar[dr] & {j}\ar[d] & &&
& & &&
& \\
& & *+[F]{k} & &&
& {k} & &&
& {k}
}
$$
\noindent
The first diagram corresponds to the full formalization.
There are eleven proof steps which are labeled $a$--$k$.
The justifications in the proof are represented by the arrows.
For instance step $h$ is justified by references to $f$ and $g$.
In Mizar syntax it would be written as `$h:\,\ldots\mbox{ \textbf{by} }f,g\,;\,$'.
%
In the second diagram six of the steps have been removed,
but the references between the steps are still present.
%If the justification checker of the system is complete, the
%correctness of this proof still can be checked, although it might
%take impractically long.
%
The third diagram corresponds to the formal proof sketch.
Now there are no labels and references to labels left.
This is generally what happens in a formal proof sketch that
mimics an informal mathematical text.
Two extreme formal proof sketches of a given formalization
are those in which all proof steps
have been removed,\footnote{
It might seem strange to call such an empty proof a `proof sketch'.
However we think it is natural to include this case in the notion
of formal proof sketch, just like $0$ is generally considered to be a natural
number, and the empty set is considered to be a set.
}
and those in which no proof steps have been removed.
These are the end points of a spectrum:\label{spectrum}
\begin{center}
\medskip
\begin{picture}(300,54)
\put(40,24){\makebox(0,0){\emph{no proofs}}}
\put(40,10){\line(0,1){8}}
\put(260,10){\line(0,1){8}}%
\put(40,14){\line(1,0){220}}%
\put(260,24){\makebox(0,0){\emph{full proofs}}}%
\put(150,0){\makebox(0,0){\textsc{formal proof sketch spectrum}}}
%\put(160,10){\line(0,1){8}}%
%\put(40,14){\line(1,0){120}}%
%\put(160,24){\makebox(0,0){\emph{full proofs}}}%
\put(120,31){\vector(0,-1){17}}
\put(120,50){\makebox(0,0){\emph{`human level'}}}
\put(120,38){\makebox(0,0){\emph{formal proof sketches}}}
\end{picture}
\medskip
\end{center}
Most systems have files that correspond to the end points.
For instance in the Coq system there are the \texttt{.g} and \texttt{.v}
files, and in the Mizar system there are the \texttt{.abs} and \texttt{.miz}
files.
Formal proof sketches give one intermediate levels of proof representation
in between these two extremes.
%Somewhere on this spectrum are the formal proof sketches that correspond
%to the prose that one finds in informal mathematical texts,
%as suggested by the arrow.
When we show formal proof sketches to people, we sometimes get the reaction
`we should build systems that can check them!'
We think it is overtly optimistic to expect that this will be possible soon.
However, as proof checking technology improves we can expect the
endpoint of `full proofs'
to get closer to the formal proof sketches at the `human level':
%Therefore the formal proof sketch spectrum will change over time:
\begin{center}
\medskip
\begin{picture}(300,54)
\put(40,24){\makebox(0,0){\emph{no proofs}}}
\put(40,10){\line(0,1){8}}
%\put(260,10){\line(0,1){8}}%
%\put(40,14){\line(1,0){220}}%
%\put(260,24){\makebox(0,0){\emph{full proofs}}}%
\put(150,0){\makebox(0,0){\textsc{formal proof sketch spectrum\rlap{ in 2048}}}}
\put(160,10){\line(0,1){8}}%
\put(40,14){\line(1,0){120}}%
\put(160,24){\makebox(0,0){\emph{full proofs}}}%
\put(120,31){\vector(0,-1){17}}
\put(120,50){\makebox(0,0){\emph{`human level'}}}
\put(120,38){\makebox(0,0){\emph{formal proof sketches}}}
\end{picture}
\medskip
\end{center}
\noindent
So formal proof sketches are too high level to be checked automatically
for mathematical correctness
(else they would be `full formalizations').
However, the notion of being a formal proof sketch is \emph{not}
an informal notion.
If someone presents you with a formal proof sketch, it is meaningful
to say that `it is correct' or `it is not correct'.
%If it is correct that person will be able show this by exhibiting a filled out
%formalization of the formal proof sketch.
%If it is not correct he or she will not be able to do so.
This is related to the proposition:
\medskip
\noindent
\textbf{Proposition. }\label{proposition}%
\emph{It is semi-decidable whether a text is a correct formal proof sketch.}
\medskip
\noindent
\textit{Proof. }%
If a text is a correct formal proof sketch, this can be shown by showing the
full formalization from which it was derived.
However, as in general it is not decidable whether
a given statement is provable in a given context,
it can in general not be decided whether a given statement with an empty
justification is a formal proof sketch. \hfill$\Box$
\section{The Proof Development Cycle}\label{section:cycle}
The development of a mathematical formalization
follows the following pattern:
\vspace{-\medskipamount}
\vspace{-\smallskipamount}
$$
\xymatrix@C=4em{
\ar@(dr,l)[rrd]|-{\txt{\em formalizing\/}} && && \\
&& *++[F]\txt{formalization}\ar@{-}@(r,r)[d]\ar@(r,dl)[rru]|-{\txt{\em presenting\/}} && \\
&& *\txt{\em editing\/}\ar@(l,l)[u] &&
}
\medskip
$$
\noindent
It is important not to forget the activity of editing a formalization.
Having a great presentation mode is not very helpful if
one needs to deal with the underlying formalization (which often is
an unclear tactic script).
If we use formal proof sketches, we can give a more detailed structure to
this development diagram:
$$
\xymatrix{
*+\txt{informal statement\strut\\of theorem}\ar[d] &&& *+\txt{formal\\`abstract'}\\
*+[F]\txt{informal\\English proof}\ar[r]\ar@{.>}@/_1pc/[rrd]|-{\txt{\em formalizing\/}} &
*+[F--]\txt{formal\\proof sketch}\ar[rd]\ar@{--}[rr] &&
*+[F--]\txt{formal\\proof sketch}\ar[u]\\
&& *+[F]\txt{full\\formalization}\ar@/_1pc/[ru]!D|(.72){\txt{\em presenting\/}} &
}
\medskip
$$
Here we present development of a formalization from an existing
informal mathematical text (as in the example from Section \ref{section:sqrt2}).
The process consists of two phases.
First, one mimics the informal English proof in the formal proof sketch language.
This is easy and fast.
Second, one `fleshes out' this formal proof sketch to a full formalization.
This generally takes much longer.
During this second phase one often discovers that the original formal
proof sketch was not correct,
and so it will change.
At the end one has a matched pair of a formal proof sketch and a full
formalization.
The full formalization then guarantees the correctness of the
mathematics, while the formal proof sketch presents it in an
understandable way.
Note that the three levels in this second diagram correspond
to the three positions on the formal proof sketch spectrum:
the top level corresponds to no proofs,
the middle level to `human level' formal proof sketches,
and the bottom level to full proofs.
%$$\xymatrix@=1.5em{
%\mbox{informal text}\ar@{->}[d] \\
%\mbox{formal proof sketch}\ar@(dr,ul)@{->}[rd] & \mbox{formal proof sketch} \\
%& \mbox{full formalization}\ar@{.}[u]
%}$$
\section{Generated Natural Language Proof}\label{section:genlang}
There are many systems to generate proofs in natural language from
formalized mathematics.
An example of such a system is the MoWGLI system from the
University of Bologna \cite{asp:weg:02}.
It generates web pages with proofs in natural language from Coq formalizations
using the following pipeline:
\begin{center}
\textbf{Coq script} $\stackrel{\sf Coq\,}{\relbar\joinrel\longrightarrow}$ Coq XML $\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ OMDoc XML $\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ \textbf{English} HTML
\end{center}
If one looks at the syntax of the output of such a system, it looks very similar
to the text that one finds in a formal proof sketch.
However, although superficially the two ways of presenting a formalization
seem very similar, there are important differences:
\begin{itemize}
\item
The systems that generate proofs in natural language \emph{automatically}
convert a formalization to a presentation.
We do not have a method to generate a (reasonable) formal proof sketch
from a full declarative formalization without human help.
%
However, one can reduce a full formalization \emph{manually} to a good
formal proof sketch, in two stages:
\begin{enumerate}
\item
The first stage is automatic: one just removes all labels
and references to labels.\footnote{
Removing \emph{all} labels might be a bit too strong
(in long proofs references sometimes can be helpful
to understand the proof)
but it is a very good first order approximation.
The number of references in informal mathematics is a tiny
fraction of the number of references in formalized mathematics.
}
This is the most important phase.
It is surprising how much more readable a Mizar text becomes
without this `visual noise'.\footnote{
Removing all linkage from a Mizar text
means removing the `\texttt{then}' keywords as well.
But of course this first stage does not need to do so too.
%(there is a choice here what to do).
In informal mathematics words like \emph{then} are often
used to link steps together.
We illustrated both styles in the example on page \pageref{example}:
in the informal layout of the formal proof sketch
we left two `then' keywords in, but in the Mizar layout we
removed them.
}
\item
The second stage consists of removing intermediate steps,
just keeping the `interesting steps' of the proof.
The problem is how to decide which steps to drop and which
to leave in.
We do not know of a good heuristic to decide this
from the structure of the proof.\footnote{
Possibly
compiler technology like \emph{basic block analysis}
is relevant for this.
}
Currently it will need manual markup of the full formalization
to mark these `interesting steps'.
Inserting that kind of markup will not be much work.
\end{enumerate}
\item
The size of generated proofs in natural
language is an order of magnitude \emph{larger} than the
size of the original formalizations,
while the size of formal proof sketches is an order of magnitude \emph{smaller}
than that of the corresponding full formalizations.
The accepted opinion seems to be that to deal with this
one should
\emph{fold} subproofs until one has something of reasonable size.
However, we doubt that this will work well.
In a procedural prover most of the steps are backward steps,
while in a declarative prover most of the steps are forward.
In both cases there will be no convenient subproofs to fold.
Of course one can write the formalizations
to combine forward and backward
steps in a way that leads to proofs with
a nice folding structure,
but that is not very practical.
And even if one would do that: our experience with Lamport-style proof
(as described in the next section) is that a subproof structure obfuscates
the `narrative' of the proof.
If one compares formal proof sketches that mimic
existing informal proofs to formal proof sketches that mimic proofs with
conveniently foldable subproofs (like Lamport-style proofs),
then the former kind has far less subproofs than
the latter kind.\footnote{%
When discussing this with Laurent Th\'ery at the TPHOLs 2003
conference, he summarized this opinion by saying
`so you like iteration but you do not like recursion'.
%That is too strong a statement, but we do claim that `informal proofs' are
%much `flatter' than one expects.
}
\end{itemize}
\section{Lamport's `How to Write a Proof'}\label{section:lamport}
Fleshing out a formal proof sketch along the formal proof sketch spectrum toward a full formalization relates to a proof format described in
Leslie Lamport's `How to Write a Proof' \cite{lam:95}.
In that paper he describes a hierarchical proof style where each
step of the proof recursively is `clarified' by a subproof until
the steps are considered to be obvious.
These `recursive proofs' apparently are very natural and seductive.\footnote{%
When discussing formalization of mathematics with Hendrik Lenstra,
he reinvented exactly this proof format on the spot.
}
Note that Lamport's proof format is \emph{not} formal.
An implementation of Lamport-style proof on the web was made in the IMP project
of Paul Cairns and Jeremy Gow \cite{cai:gow:03}.
They have course notes in topology as a set of web pages.
On each of these pages is both an informal proof as well as a Lamport-style
proof in which subproofs can be collapsed by clicking on buttons.
We compared one of these web pages to our approach:
we created formal proof sketches
both for the informal proof as well as for the Lamport-style proof.
%The Mizar language turned out to be flexible enough to
%easily accommodate both of these proof styles.
Our experience was that the first formal proof sketch was the more
understandable of the two.
We had the impression that
having many subproofs does obscure the structure of a proof
rather than clarify it.
It should be clear that we do not claim that it is bad to have lemmas
to isolate important parts of proofs.
Subproofs certainly have their place on the lemma level.
However, having them on the micro-level of the proofs steps
seems not to be very helpful.
Interestingly, when doing this experiment
we found that without adding steps
the Lamport-style proof was not detailed enough
to be accepted by the Mizar system,
and when we added that detail it turned out that that it contained some mistakes.
%So much for the informal approach of Lamport-style proof.
\section{Proof Obligations for Automated Theorem Provers}\label{section:atp}
The justifications in a formal proof sketch cannot be checked by the
computer because the steps are too large and because there are not enough references.
If one does not remove the references (i.e., one takes the formal proof
sketch that corresponds to the middle graph on page \pageref{graph}),
then one might consider the inferences that need
to be justified.
For the example from Section \ref{section:sqrt2} all but one inference turn
out to be a simple algebraic problem:
\begin{center}
\begin{tabular}{rrcll}
\llap{1$\rightarrow$\qquad}& $\displaystyle b\ne 0 \;\land\; \sqrt{2} = {a/b}$ & $\;\vdash\;$ & $a^2 = 2 b^2$ & $\qquad$\\
\noalign{\smallskip}
\llap{2$\rightarrow$\qquad}& $b\in\Z \;\land\; a^2 = 2 b^2$ & $\;\vdash\;$ & $2\,|\,a^2$\\
\noalign{\smallskip}
\llap{3$\rightarrow$\qquad}& $a\in\Z \;\land\; 2\,|\,a^2$ & $\;\vdash\;$ & $2\,|\,a$\\
\noalign{\smallskip}
\llap{5$\rightarrow$\qquad}& $a^2 = 2 b^2 \;\land\; a = 2c$ & $\;\vdash\;$ & $4 c^2 = 2 b^2$\\
\noalign{\smallskip}
\llap{6$\rightarrow$\qquad}& $4 c^2 = 2 b^2$ & $\;\vdash\;$ & $2 c^2 = b^2$\\
\noalign{\smallskip}
\llap{7$\rightarrow$\qquad}& $b\in\Z \;\land\; c\in\Z \;\land\; 2 c^2 = b^2$ & $\;\vdash\;$ & $2\,|\,b$\\
\noalign{\smallskip}
\llap{8$\rightarrow$\qquad}& $(a,b) = 1 \;\land\; 2\,|\,a \;\land\; 2\,|\,b$ & $\;\vdash\;$ & $\bot$
\end{tabular}
\end{center}
The Mizar notion of inference (called `obviousness') is rather weak,
and therefore it is
interesting to give these problems -- together with the relevant lemmas --
to a complete first order prover (if it runs long enough and
with enough memory it eventually will find a justification, if it exists).
As an experiment we gave these problems\footnote{%
Conversion from Mizar justifications to first order problems in TPTP format
was kindly done for us by Josef Urban of Charles University in Prague.
}
to the Meson prover of the HOL system \cite{har:96:1}.
The results were rather disappointing
(the table also shows the number of steps that the Meson prover needed
to solve the problems that it could solve):
\begin{center}
\begin{tabular}{rcccrrr}
&& $\quad\mbox{\em Mizar\/}\quad$ & {\em Meson\/} &&& $\qquad$ \\
$\qquad 1\mathord{\rightarrow}\quad$ && $-$ & $-$ && \\
$2\mathord{\rightarrow}\quad$ && $+$ & $+$ & 61 & $\quad$1.49$\,${\em s} \\
$3\mathord{\rightarrow}\quad$ && $+$ & $+$ & 20 & 0.14$\,${\em s} \\
$4\mathord{\rightarrow}\quad$ && $+$ & $+$ & 142 & 1.02$\,${\em s}\\
$5\mathord{\rightarrow}\quad$ && $-$ & $-$ && \\
$6\mathord{\rightarrow}\quad$ && $-$ & $-$ && \\
$7\mathord{\rightarrow}\quad$ && $-$ & $+$ & $\quad$18839 & 4.71$\,${\em s} \\
$8\mathord{\rightarrow}\quad$ && $-$ & $-$ &&
\end{tabular}
\end{center}
We claim that justification problems
taken from formal proof sketches of existing mathematical
proofs are a good target for the automated theorem proving
community.
In contrast, current
problem sets for automated theorem provers like TPTP \cite{sut:sut:yem:94}
are mathematically mostly not very interesting.
%
Of course we would like our automated theorem provers to be
able to solve non-trivial problems,
but first they should be able to solve the problems that
humans consider to be sufficiently trivial that they do not need any
words in an informal proof.
\section{Two More Examples}\label{section:examples}
In Section \ref{section:sqrt2} we showed that a formal proof
sketch of an informal mathematical proof can closely
mimic the original.
We think that this is generally the case:
\medskip
\noindent
\textbf{Claim. }\emph{Most existing informal proofs can be faithfully mimicked as a Mizar formal proof sketch.}
\medskip
\noindent
We have experimented with formal proof sketches of various existing proofs
and in our experience this claim seems justified.
In this section we will show two more examples.
The first is a proof that was on a slide of the talk
`Formalizing an intuitionistic proof of the Fundamental
Theorem of Algebra' by
Herman Geuvers at the 7th Dutch Proof Tools Day in Utrecht.
The slide called it a `romantic proof', in contrast to
the `cool proofs' of formalized mathematics.
(To highlight the correspondence to the formal proof sketch, we
underlined two random phrases of the proof.)
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
{\sc Theorem}$\,$ \underbar{There are infinitely many primes:}\\
for every number $n$ there exists a prime $p> n$ \medskip
\medskip\noindent
\textsc{Proof} [after Euclid]\\
Given $n$. Consider $k=n!+1$, where $n!=1\cdot 2\cdot 3\cdot \ldots\cdot n$.\\
\underbar{Let $p$ be a prime that divides $k$.}\\
For this number $p$ we have $p> n$: otherwise $p\leq n$;\\
but then $p$ divides $n!$,\\
so $p$ cannot divide $k=n!+1$,\\
contradicting the choice of $p$. QED
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
And here is the corresponding Mizar formal proof sketch:
%(with the corresponding two phrases underlined):
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
{\sc theorem}$\,$ \underbar{$\{n: n\mbox{\rm\ is prime}\}$ is infinite} $\,${\sc proof}\\
for $n$ ex $p$ st $p$ is prime \& $p > n$
\medskip\noindent
{\sc proof} :: [after Euclid]\\
let $n$; set $k = n! + 1$;\\
\underbar{consider $p$ such that $p$ is prime \& $p$ divides $k$;}\\
take $p$; thus $p$ is prime; thus $p > n$ $\,${\sc proof}$\,$ assume $p <= n$;\\then $p$ divides $n!$;\\
not $p$ divides $n! + 1$;\\
thus contradiction; $\,${\sc end; end;} thus thesis; {\sc end;}
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
The other example is from Rob Nederpelt's report on Weak Type Theory \cite{ned:01}:
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
{\sc Theorem.} Let $G$ be a set with a binary operation $\cdot$ and \underbar{left unit ele-} \underbar{ment
$e$.} Let $H$ be a set with binary operation $*$ and assume that $\phi$ is a homo%-
morphism of $G$ onto $H$. Then $H$ has a left unit element as well.
\medskip\noindent
{\sc Proof.} Take $e' = \phi(e)$. Let $h\in H$. \underbar{There is $g\in G$ such that $\phi(g) = h$.}
Then $$e' * h = \phi(e) * \phi(g) = \phi(e\cdot g) = \phi(g) = h,$$
hence $e'$ is left unit element of $H$.\hfill$\Box$
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
And here is the corresponding formal proof sketch of this simple proof:
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
%\quad
let $G,H$ be non empty HGrStr;
\underbar{let $e$ be Element of $G$ such that $e$ is\_left\_}\break\underbar{unit\_of $G$;}
let {\it phi\/} be map of $G,H$ such that
{\it phi\/} is\_homomorphism $G,H$ and {\it phi\/} is onto;
thus ex $e'$ being Element of $H$ st $e'$ is\_left\_unit\_of $H$\medskip\\
{\sc proof}$\,$
take $e' = \mbox{\it phi\/}.e$;
now
let $h$ be Element of $H$;
\underbar{consider $g$ being} \underbar{Element of $G$ such that $\mbox{\it phi\/}.g = h$;}
thus
$$\mbox{$e' * h = \mbox{\it phi\/}.e * \mbox{\it phi\/}.g \mathrel{\mbox{.=}} \mbox{\it phi\/}.(e * g) \mathrel{\mbox{.=}} \mbox{\it phi\/}.g \mathrel{\mbox{.=}} h$;}$$
end;
hence $e'$ is\_left\_unit\_of $H$;
\hfill {\sc end;}
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\section{Conclusion}
\subsection{Discussion}
In Section \ref{section:problem} we listed two problems with
formalization of mathematics:
The first problem was that formalized mathematics does not
look much like ordinary mathematical text.
We think that the notion of formal proof sketch is a step toward
a solution of this problem.
The second problem was that formalization of mathematics
is too much work.
We think that by not fully formalizing a proof,
but just using formal proof sketches for the interesting
parts,
we have an approach that is between no check at all and
full verification of the correctness.
In the formal proof sketch we will be able to write
the interesting parts of the proof (like in Lamport's approach)
and the system will check those parts,
while we do not have to spend time on the trivial details
that take most of the time.
\subsection{Related Work}
%In the NuPRL system it is possible
%to present proofs by showing the statements from the goals interleaved
%with the tactics from the proof script.
%One can `group' the tactics to get
%a presentation that can be considered to be a `formal proof sketch
%for the NuPRL system.'
%However, with a tactic based prover like NuPRL it is not
%easy to write such a `formal proof sketch' {\em before\/} working out the
%full formalization.
%Also, the proof presentation is less close to an English language
%version of the proof than is possible with a declarative system like Mizar.
Rob Nederpelt
has a language called {\em weak type theory\/} or WTT \cite{ned:01},
for writing formal mathematics in a way that is
closer to informal
mathematics than currently is the case in formal systems.
It is basically a formalization language where steps in the proofs
are just stated but not checked.
WTT texts are similar to formal proof sketches
(they might be considered the formal proof sketches of the Automath language),
but there are several big differences.
Although it is structurally similar to informal mathematics,
a WTT text does not at all resemble the way informal
mathematics looks.
Also, there is no notion of mathematical correctness for a WTT
text (there is only a notion of `weak type correctness').
Finally there is currently no way to relate a WTT text to
a full formalization of the same mathematics.
Laurent Th\'ery describes in \cite{the:03} a proof
representation (which he there calls `proof format')
that is similar to what we call a formal proof sketch here.\footnote{%
We both seemed to be unaware of each other's work when we were
doing it (a preliminary paper about formal proof
sketches \cite{wie:03:1} was only available to the attendees
of the 7th Dutch Proof Tools Day in Utrecht), and we only found out about
the similarities in each other's work at the UITP workshop in Rome.
}
%
Nevertheless, his approach differs in some important
respects from ours:
\begin{itemize}
\item
In \cite{the:03} there are three very different proofs languages:
the XML file that contains the `formal proof sketch' inside the machine,
the natural language presentation with which this file is shown in the interface,
and the Coq file that holds the proof obligations that have to be proved.
In our approach we use the Mizar language for both the formal proof sketch
and for the full formalization,
and therefore in our approach all these three languages coincide,
giving a much more integrated whole.
\item
In \cite{the:03} there are \emph{two} levels: the XML level and the
Coq level.
In our approach there is a \emph{spectrum} of related formal proof sketches (see page \pageref{spectrum} below).
\item
In our approach it is possible to take a full Mizar formalization and
systematically reduce it to a formal proof sketch.
In the approach from \cite{the:03} there is no similar way
to turn a Coq formalization into anything similar to a formal proof sketch.
\item
We `reuse' the language of a full-fledged system for our formal
proof sketches.
Therefore we have a much richer language than
the system from \cite{the:03}.
Especially we get the full Mizar type system, which is very mathematical.
Also we get features in our language like definitions,
proof by cases and iterated equalities.
\item
Finally, the correctness of the natural deduction `skeleton' steps in
our formal proof sketches
are checked by Mizar
with respect to the structure of the current goal,
in contrast with \cite{the:03}
where even that kind of checking is considered a proof obligation
to be handled later.
(An example of this kind of checking occurs when the goal is of the
form $A\to B$ and the step says `\emph{assume} $A$'.)
\end{itemize}
\subsection{Future Work}
Formal proof
sketches should be integrated into a proof development environment.
The same proof language should be used
for the formal proof sketches and for the full formalizations.
%
In that system one should then try to mimic
the proofs of a non-trivial existing
mathematical text (like for instance a chapter from a textbook)
as a sequence of formal proof sketches.
This will be a good test for the formal proof sketch
approach in practice.
\medskip
\paragraph{Acknowledgments.}
Thanks to
Henk Barendregt,
Herman Geuvers,
John Harrison,
Joe Hurd,
Paul Jackson,
Hendrik Lenstra,
Rob Nederpelt,
Claudio Sacerdoti Coen,
Bart de Smit,
Bas Spitters,
Dan Synek
and
Laurent Th\'ery
for stimulating discussions on the subject of this paper.
Thanks also to the anonymous referees for helpful comments.
%\bibliographystyle{plain}
%\bibliography{frk}
\begin{thebibliography}{10}
\bibitem{asp:weg:02}
A.~Asperti and B.~Wegner.
\newblock {MOWGLI -- A New Approach for the Content Description in Digital
Documents}.
\newblock In {\em {Proc. of the 9th Intl. Conference on Electronic Resources
and the Social Role of Libraries in the Future}}, volume~1, Autonomous
Republic of Crimea, Ukraine, 2002.
\bibitem{cai:gow:03}
Paul Cairns and Jeremy Gow.
\newblock {A Theoretical Analysis of Hierarchical Proofs}.
\newblock In Andrea Asperti, Bruno Buchberger, and James Davenport, editors,
{\em Mathematical Knowledge Management, Proceedings of MKM 2003}, volume 2594
of {\em LNCS}, pages 175--187. Springer, 2003.
\bibitem{har:wri:60}
G.H. Hardy and E.M. Wright.
\newblock {\em An Introduction to the Theory of Numbers}.
\newblock Clarendon Press, Oxford, fourth edition, 1960.
\bibitem{har:96:1}
John Harrison.
\newblock {Optimizing Proof Search in Model Elimination}.
\newblock In M.~A. McRobbie and J.~K. Slaney, editors, {\em 13th International
Conference on Automated Deduction}, volume 1104 of {\em LNCS}, pages
313--327, New Brunswick, NJ, 1996. Springer-Verlag.
\bibitem{lam:95}
Leslie Lamport.
\newblock {How to Write a Proof}.
\newblock {\em American Mathematical Monthly}, 102(7):600--608, 1995.
\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock \url{}.
\bibitem{ned:01}
Rob Nederpelt.
\newblock {Weak Type Theory, a formal language for mathematics}.
\newblock Technical Report 02-05, Eindhoven University of Technology,
Department of Math.~and Comp.~Sc., May 2002.
\bibitem{sut:sut:yem:94}
Geoff Sutcliffe, Christian Suttner, and Theodor Yemenis.
\newblock The {TPTP} problem library.
\newblock In Alan Bundy, editor, {\em Proc.\ 12th Conference on Automated
Deduction {CADE}, Nancy/France}, pages 252--266. Springer-Verlag, 1994.
\bibitem{sym:99}
Don Syme.
\newblock {Three Tactic Theorem Proving}.
\newblock In {\em Theorem Proving in Higher Order Logics, TPHOLs '99, Nice,
France}, volume 1690 of {\em LNCS}, pages 203--220. Springer, 1999.
\bibitem{the:03}
Laurent Th\'ery.
\newblock {Formal Proof Authoring: an Experiment}.
\newblock In Christoph L{\"u}th and David Aspinall, editors, {\em UITP 2003,
Rome, Technical Report No. 189, Institut f{\"u}r Informatik, Albert-Ludwigs
Universit{\"a}t}, pages 143--159, Freiburg, September 2003.
\bibitem{wen:02}
M.~Wenzel.
\newblock {\em {Isabelle/Isar --- a versatile environment for human-readable
formal proof documents}}.
\newblock PhD thesis, {Institut f\"ur Informatik, Technische Universit\"at
M\"unchen}, 2002.
\newblock
\url{}.
\bibitem{wie:99:1}
F.~Wiedijk.
\newblock {Mizar: An Impression}.
\newblock
\url{},
1999.
\bibitem{wie:03:1}
F.~Wiedijk.
\newblock {Formal proof sketches}.
\newblock In Wan Fokkink and Jaco van~de Pol, editors, {\em 7th Dutch Proof
Tools Day, Program + Proceedings}, Amsterdam, 2003. CWI.
\newblock \url{}.
\end{thebibliography}
\end{document}