\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}