\documentclass[runningheads]{llncs} \usepackage[all]{xypic} \usepackage{latexsym,amssymb} \raggedbottom \def\Z{{\mathbb Z}} \def\toolong{$\hspace{-3.2cm}$} \begin{document} \title{Formal proof sketches} \author{Freek Wiedijk} \institute{University of Nijmegen} \maketitle \begin{abstract} We define the notion of {\em formal proof sketch\/} for the mathematical language Mizar. We show by examples that formal proof sketches are very close to informal mathematical proofs. We discuss some ways in which formal proof sketches might be used to improve mathematical proof assistants. \end{abstract} \section{Introduction} \subsection{Problem} Large mathematical formalizations are often difficult to understand. They generally consist of several files, each containing a long series of definitions and lemmas, with for each lemma a proof which is a maze of steps. As such, they are like large computer programs, which consist of several files, each containing a long series of declarations and functions, with for each function an implementation which is a maze of statements. However the analogy is not perfect. It is much easier to follow the steps through the implementation of a program than to follow the steps through the formalization of a theorem. There are two levels on which it is difficult to understand a large mathematical formalization. It is difficult to understand the overall structure of the formalization, i.e., to know what are the important definitions and lemmas and in which files to find them. And it is difficult to find one's way through the formal proof of a lemma, i.e., to understand what the structure of that proof is. In this note we address this second difficulty. Something that makes a formalization easier to understand, does not necessarily make it easier to create. The approach presented in this note makes it easier to read a mathematical formalization, but it will not make it easier to write one. This means that the representation of proofs that this note proposes are {\em not\/} meant to be a `better way' for writing a formal proof. A representation that can be checked by machine is much more involved than the representation that we study here, and it will be as difficult to write as ever. In other words, our work is on right hand side of the following diagram:\vspace{-6pt} $$ \xymatrix@C=4em{ \ar@(dr,l)[rrd]|-{\txt{\em formalizing\/}} && && \\ && *++[F]\txt{formalization}\ar@(r,dl)[rru]|-{\txt{\em presenting\/}} && } \medskip $$ and it is not especially relevant for the left hand side. Here are some of the main ways to present a formalization in such a way that it becomes easier to understand for a human: \begin{itemize} \item {\em Removing the proofs.} For instance in the Coq system one can generate a so-called `\verb|.g|' file, which is just the Coq input script with the proofs removed. Likewise, in the Mizar system one generates so-called `abstracts', again just the formalizations with all proofs removed. \item {\em Rendering the formulas with mathematical symbols.} For instance in the prover interface Proof General one can use the X-Symbols feature of emacs, showing mathematical symbols instead of ASCII strings. In a similar approach, the Theorema system uses the Mathematica front-end to present its formulas in mathematical style. Some systems (like Agda and NuPRL) even have a full-fledged structure editor that displays mathematical formulas in a structural way. \item {\em Generating natural language text from the formalization.} \item {\em Merging natural language text with the formalization in the spirit of `literate programming'.} \end{itemize} Generally the problem with a formal proof is that it is big (because the steps are small), and that one looses grip on the whole because of this. The last two approaches in this list tend to make a formalization even bigger. In contrast with this we believe that to make a formalization accessible, one has to make it smaller. Many people think that in order to make a formalization easier to understand, one has to transform it. However this means that one creates distance between the formalization and its presentation. This can be a problem if we add a third arrow to the diagram:\vspace{-6pt} $$ \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] && } \smallskip $$ To be able to successfully edit a formalization, one has to look at the presentation (in order to be able to understand it), but one also has to work in the underlying formalization itself (because that is where things really happen). If those two versions of the proof differ too much, then the presentation does not help. In that case, for a user who just understands the presentation, the formalization will be a static thing (because it cannot easily be modified) instead of a `living proof'. Therefore, we claim that the presentation should be as close to the original formalization as possible. In this paper we are looking for a presentation of a formalization which is: \begin{itemize} \item {\em Shorter than the full formalization}, in the sense that the most trivial details of the proof are not shown. \item {\em Close to the full formalization}, in the sense that it is easy to go back and forth between the two and to find matching locations in both versions. \end{itemize} \subsection{Approach} We introduce the notion of {\em formal proof sketch}. A formal proof sketch is a notion related to the mathematical language Mizar \cite{muz:93,wie:99:1}. A formal proof sketch is a completely correct Mizar text, apart from errors \verb|*4| and \verb|*1|. These errors say that reasoning steps are not justified. (Therefore, in a formal proof sketch one can leave out all labels and justifications to make it more readable.) A formal proof sketch falls between a formalization with full proofs and an abstract with all proofs removed. In a formal proof sketch some of the steps, as well as the connections between the steps, have been removed. A formal proof sketch is called {\em correct}, if one can add labels, justifications and steps to it, in such a way that one gets a correct Mizar formalization. We call such a formalization the {\em completion\/} of the sketch. Being correct is a semi-decidable notion. If a sketch is correct one can show so by exhibiting a completion, but if it is not, there is no guaranteed way to find out. The observation of this note is that, given an informal natural language proof, it is possible to write a correct formal proof sketch which is linguistically very close to it. In this note we will show two examples of this, one in Section~\ref{sketch}, and one in Section~\ref{geomath}. The process of formalizing an informal proof, and then presenting it through a formal proof sketch, is represented in the following 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 $$ For our first example the informal English proof and the formal proof sketch are in Section~\ref{sketch}, while the full formalization is in Section~\ref{full}. For our second example, all three representations are next to each other in Section~\ref{geomath}. When completing a formal proof sketch into a full formalization, sometimes one modifies the structure of the proof a bit. This makes the formal proof sketch change too: hence the two boxes for the formal proof sketch in the diagram. We show an example of such a change in Section~\ref{geomath}. \subsection{Related Work} Rob Nederpelt has a language called {\em weak type theory\/} or WTT \cite{ned:01}, that is meant to formalize mathematics in a way that is closer to natural language than currently is the case in formal systems. It is basically a formalization language like the others, but without any proofs. We are not convinced that having a separate language for this purpose is desirable or even necessary. To us Mizar abstracts (which also are formalizations without proofs) are at least as readable as Nederpelt's WTT formalizations. Paul Jackson told us that in the NuPRL community it is customary to present proofs by showing the statements from the goals interleaved with the tactics from the proof script. To improve the presentation one then `groups' the tactics and gets a much shorter presentation. This is very similar to what we describe in this note. The main difference is that in the case of NuPRL it is not easy to write the proof sketch {\em before\/} working out the full formalization. In the case of Mizar it is. Another difference is that in the case of Mizar the result is much closer to that informal English version of the proof than in NuPRL. \subsection{Contribution} Our contribution is twofold: \begin{itemize} \item We note that it is possible to get very close to informal mathematical English using Mizar syntax, as long as one does not mind omitting justifications for the steps. \item We note that one can give a formal definition of a notion called {\em formal proof sketch\/} for this. (Note that in this note we do not give this formal definition, but it does exist.) \end{itemize} \subsection{Outline} The plan of the paper: in Section~\ref{sketch} we present an informal English proof with its formal proof sketch approximation. In Section~\ref{typography} we discuss how the typographical differences obfuscate the similarity of those two versions of the proof. In Section~\ref{full} we give the full Mizar formalization of the proof. In Section~\ref{meson} and Section~\ref{algebra} we study whether we can make the full formalization be closer to the formal proof sketch by using a complete first order prover (instead of the restricted inference engine of Mizar) and by using computer algebra. In Sections~\ref{dual} and \ref{folding} we look at possibilities of using formal proof sketches in the interface of a proof assistant. Finally, in Section~\ref{geomath} we present a second example of a formal proof sketch. \section{A formal proof sketch}\label{sketch} In Hardy and Wright's {\em An Introduction to the Theory of Numbers\/} \cite{har:wri:60}, the irrationality of $\sqrt{2}$ is proved on pp.~39--40 in the following way: \begin{quote} {\sc Theorem 43 (Pythagoras' theorem).} {\em $\sqrt{2}$ is irrational.} \medskip 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$ \end{quote} If one writes this text in Mizar syntax, it turns out to be almost identical: \begin{center} \begin{tabular}{ll} \verb|theorem Th43: sqrt 2 is irrational| & \\ \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} \end{center} With an appropriate \verb|environ| header, this is correct Mizar, except for eight `reasoning errors', as indicated by the numbered arrows. We call such a Mizar text that only has reasoning errors a formal proof sketch. \section{Comparing typography}\label{typography} The informal proof and the corresponding formal proof sketch are more similar than might seem at a first glance, because one of them is printed as natural language in a text font, while the other is printed with one step per line in a typewriter font. To stress the similarity of the texts, here they are next to each other: \begin{center} \begin{tabular}{rcl} {\sc Theorem 43\rlap{.}} & $\quad$ & {\verb|theorem Th43:|} \\ {\em $\sqrt{2}$ is irrational\rlap{.}} && {\verb| sqrt 2 is irrational|} \\ && {\verb|proof|} \\ If $\sqrt{2}$ is rational\rlap{,} && {\verb| assume sqrt 2 is rational;|} \\ then the equation && {\verb| consider a,b such that|} \\ {(4.3.1)}\quad $a^2 = 2b^2$\quad is soluble in && {\verb|4_3_1: a^2 = 2*b^2 and|} \\ integers $a$, $b$ with $(a,b) = 1$\rlap{.} && {\verb|A1: a,b are_relative_prime;|} \\ Hence $a^2$ is even\rlap{,} && {\verb| a^2 is even;|} \\ and therefore $a$ is even\rlap{.} && {\verb| a is even;|} \\ If $a = 2c$\rlap{,} && {\verb| consider c such that a = 2*c;|} \\ then $4c^2 = 2b^2$\rlap{,} && {\verb| 4*c^2 = 2*b^2;|} \\ $2c^2 = b^2$\rlap{,} && {\verb| 2*c^2 = b^2;|} \\ and $b$ is also even\rlap{,} && {\verb| b is even;|} \\ contrary to the hypothesis && {\verb| thus contradiction|} \\ that $(a,b) = 1$\rlap{.} && {\verb| by A1;|} \\ $\Box\!$ && {\verb|end;|} \end{tabular} \end{center} On the left there is the Hardy \& Wright original, on the right is the formal proof sketch translation. % We also can write the `Mizar' of the formal proof sketch in `natural language typography' like this: \begin{quote} {\sc Theorem}\enskip {\em $\sqrt 2$ is irrational.} \medskip {\sc Proof}\enskip Assume $\sqrt 2$ is rational. Then consider $a,b$ such that $$a^2 = 2 b^2$$ and $a,b$ are relative prime. $a^2$ is even. Then $a$ is even. Then consider $c$ such that $a = 2 c$. $4 c^2 = 2 b^2$. Then $2 c^2 = b^2$. Then $b$ is even. Hence contradiction. $\hfill\Box$ \end{quote} This text exactly follows the Mizar syntax. The only changes are that the formulas have been written with symbols and that the capitalization and punctuation has been modified slightly. \section{The full proof}\label{full} If we `fill out' the formal proof sketch from Section~\ref{sketch} to a full Mizar article, we get: \begin{quote} \underbar{\tt{theorem Th43: sqrt 2 is irrational}} \\ \underbar{\tt{proof}} \\ \verb| |\underbar{\tt{assume sqrt 2 is rational;}} \\ \verb| then |\underbar{\tt{consider a,b such that}} \\ \verb|B1: b <> 0 and| \\ \verb|B2: sqrt 2 = a/b and| \\ \verb|A1: |\underbar{\tt{a,b are\_relative\_prime}}\verb| by Def1|\underbar{\tt{;}} \\ \verb|B3: b^2 <> 0 by B1,SQUARE_1:73;| \\ \verb| 2 = (a/b)^2 by B2,SQUARE_1:def 4| \\ \verb| .= a^2/b^2 by SQUARE_1:69;| \\ \verb| then| \\ \underbar{\tt{4\_3\_1: a\^{}2 = 2*b\^{}2}}\verb| by B3,REAL_1:43|\underbar{\tt{;}} \\ \verb| a^2 is even by 4_3_1,ABIAN:def 1;| \\ \verb| then| \\ \verb|A2: |\underbar{\tt{a is even}}\verb| by PYTHTRIP:2|\underbar{\tt{;}} \\ \verb| then |\underbar{\tt{consider c such that}} \\ \verb|A3: |\underbar{\tt{a = 2*c}}\verb| by ABIAN:def 1|\underbar{\tt{;}} \\ \verb|B4: |\underbar{\tt{4*c\^{}2 =}}\verb| (2*2)*c^2| \\ \verb| .= 2^2*c^2 by SQUARE_1:def 3| \\ \verb| .= |\underbar{\tt{2*b\^{}2}}\verb| by A3,4_3_1,SQUARE_1:68|\underbar{\tt{;}} \\ \verb| 2*(2*c^2) = (2*2)*c^2 by AXIOMS:16| \\ \verb| .= 2*b^2 by B4;| \\ \verb| then |\underbar{\tt{2*c\^{}2 = b\^{}2}}\verb| by REAL_1:9|\underbar{\tt{;}} \\ \verb| then b^2 is even by ABIAN:def 1;| \\ \verb| then |\underbar{\tt{b is even}}\verb| by PYTHTRIP:2|\underbar{\tt{;}} \\ \verb| then 2 divides a & 2 divides b by A2,Def2;| \\ \verb| then| \\ \verb|B5: 2 divides a gcd b by INT_2:33;| \\ \verb| a gcd b = 1 by A1,INT_2:def 4;| \\ \verb| |\underbar{\tt{hence contradiction}}\verb| by B5,INT_2:17|\underbar{\tt{;}} \\ \underbar{\tt{end;}} \end{quote} In this, the formal proof sketch parts have been underlined. This proof needs two `lemmas' (in the form of redefinitions) that are not present in the Mizar library: \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} and: \begin{quote} \begin{verbatim} redefine attr a is even means :Def2: 2 divides a; \end{verbatim} \end{quote} \section{Bigger steps from a stronger first order prover}\label{meson} One can show the relation between the full proof and the formal proof sketch by studying relations between graphs. We draw graphs in which the steps of a proof are represented by the vertices, and where justifications are represented by the edges. The graph that we give here is not the graph of the example (that one would be too big), but a simplified version of the upper part of it. The graph on the left corresponds to the full article. The steps that are in the formal proof sketch as well, have been put in boxes. The graph on the right corresponds to the formal proof sketch. The graph in the middle is an intermediate version: here the appropriate connections have been left in. These justifications are too `big' for Mizar to be verified. If Mizar inferences would be allowed to be arbitrarily difficult first order inferences, the article corresponding to this graph would be correct Mizar. $$ \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} } $$ The Mizar text for the example that corresponds to the middle graph is: \begin{center} \begin{tabular}{ll} \verb|theorem Th43: sqrt 2 is irrational| & \\ \verb|proof| & \\ \verb| assume sqrt 2 is rational;| & \\ \verb| then consider a,b such that| & \\ \verb|4_3_1: a^2 = 2*b^2 and| & \\ \verb|A1: a,b are_relative_prime by Def1,SQUARE_1:73,| & \\ \verb| SQUARE_1:def 4,SQUARE_1:69,REAL_1:43;| & \rlap{\quad$\mathord{\leftarrow}1$} \\ \verb| a^2 is even by 4_3_1,ABIAN:def 1;| & \rlap{\quad$\mathord{\leftarrow}2$} \\ \verb| then| & \\ \verb|A2: a is even by PYTHTRIP:2;| & \rlap{\quad$\mathord{\leftarrow}3$} \\ \verb| then consider c such that| & \\ \verb|A3: a = 2*c by ABIAN:def 1;| & \rlap{\quad$\mathord{\leftarrow}4$} \\ \verb| 4*c^2 = 2*b^2 by A3,4_3_1,SQUARE_1:def 3,SQUARE_1:68;| & \rlap{\quad$\mathord{\leftarrow}5$} \\ \verb| then 2*c^2 = b^2 by AXIOMS:16,REAL_1:9;| & \rlap{\quad$\mathord{\leftarrow}6$} \\ \verb| then b is even by ABIAN:def 1,PYTHTRIP:2;| & \rlap{\quad$\mathord{\leftarrow}7$} \\ \verb| hence contradiction by A1,A2,ABIAN:def 1,INT_1:def 9,| & \\ \verb| INT_2:33,INT_2:def 4,INT_2:17;| & \rlap{\quad$\mathord{\leftarrow}8$} \\ \verb|end;| \end{tabular} \end{center} The lists of references to theorems in the justifications get quite long, because the justifications of several steps have been `put together'. In practice determining those lists is as much work as doing the intermediate steps one-selves. Therefore no-one would write a proof like this, even if Mizar could justify arbitrarily big first order steps. Still it is interesting to see how well a full first order prover can do on these steps. The HOL Light system by John Harrison \cite{har:00} implements a full first order prover called \verb|MESON_TAC|. We gave the first order problems corresponding to the eight inference steps to this prover. The steps in TPTP format were provided to us by Josef Urban. The result of this test was: \begin{center} \begin{tabular}{rcccrr} && $\quad\mbox{\em Mizar\/}\quad$ & {\em Meson\/} && \\ $\qquad 1\mathord{\rightarrow}$ && $-$ & $-$ && \\ $2\mathord{\rightarrow}$ && $+$ & $+$ & 61 & $\quad$1.49$\,${\em s} \\ $3\mathord{\rightarrow}$ && $+$ & $+$ & 20 & 0.14$\,${\em s} \\ $4\mathord{\rightarrow}$ && $+$ & $+$ & 142 & 1.02$\,${\em s}\\ $5\mathord{\rightarrow}$ && $-$ & $-$ && \\ $6\mathord{\rightarrow}$ && $-$ & $-$ && \\ $7\mathord{\rightarrow}$ && $-$ & $+$ & $\quad$18839 & 4.71$\,${\em s} \\ $8\mathord{\rightarrow}$ && $-$ & $-$ && \end{tabular} \end{center} The last two columns are number of inferences for the step and the time it took to find those inferences. For the steps for which HOL Light could not find a justification, we let \verb|MESON_TAC| run for at least an hour on a 1$\,$GHz machine, and we let it try at least ten million inferences. Surprisingly, although the first order prover in HOL Light can {\em in theory\/} do arbitrarily complicated first order problems, {\em in practice\/} it does about as well as Mizar. \section{Bigger steps from computer algebra}\label{algebra} Most of the eight `problems' from the previous section do not involve logical quantifiers, but are basically algebraic in character: \begin{center} \begin{tabular}{rrcl} \llap{1$\rightarrow$\qquad}& $\displaystyle b\ne 0 \;\land\; \sqrt{2} = {a\over b}$ & $\;\vdash\;$ & $a^2 = 2 b^2$\\ \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{\bigskip} \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 omitted fourth step (and the omitted part of the first step) involves an existential quantifier. It is not practical to use a first order reasoning tool to find the steps to get from $a^2 = 2b^2$ and $a = 2c$ to $4 c^2 = 2 b^2$. This is a problem to be solved algorithmically, and not by searching. To be able to be allowed steps like this in a formalization, one would like to have an algebraic decision procedure that knows about the notions in these inferences. If one had such a decision procedure, one would be able to get closer to the formal proof sketch. \section{Hyperlinks between formal proof sketch and full formalization}\label{dual} We will now turn to the question of how to integrate formal proof sketches into an interface to make a formalization more accessible. The simplest is to put two windows next to each other in the interface: one with the full formalization and one with the formal proof sketch. In such an interface it would be nice if those two windows were `synchronized' in such a way that when scrolling one, the corresponding part of the other always appear next to it. Alternatively one could have `hyperlinks' between the two representations to easily go from a position in the one to the corresponding position in the other. In such an interface the underlined parts of the proof from Section~\ref{full} would be links to the corresponding place in the abstract. One would like to have a tool to {\em extract\/} a formal proof sketch from a Mizar formalization. For that one would like to have some syntax in the Mizar language to `mark' the steps that should appear in the formal proof sketch. Such a tool has to be a bit subtle, because it should also extract all constructions like `\verb|let|', `\verb|consider|' and `\verb|set|' which introduce variables that are used in the extracted steps in the formal proof sketch. \section{Folding in the interface}\label{folding} Alternatively one could have only one window, with a `folding interface'. On request of the user some parts of the full formalization might be `hidden', to make the text look more like the formal proof sketch, and therefore easier to understand. The naive way to do this, is to complete the formal proof sketch with {\em subproofs\/} and then hide the subproofs on request. That way the proof will look like: %\def\foldedproof#1{$\spadesuit_{#1}$} \def\foldedproof#1{$\,\ldots\,$} \begin{quote} \verb|theorem Th43:|\\ \verb| sqrt 2 is irrational|\\ \verb|proof|\\ \verb| assume|\\ \verb|C1: sqrt 2 is rational;|\\ \verb| |\foldedproof{1}\verb|; then consider a,b such that|\\ \verb|4_3_1: a^2 = 2*b^2 and|\\ \verb|A1: a,b are_relative_prime;|\\ \verb| a^2 is even by 4_3_1,ABIAN:def 1;|\\ \verb| then|\\ \verb|A2: a is even by PYTHTRIP:2;|\\ \verb| then consider c such that|\\ \verb|A3: a = 2*c by ABIAN:def 1;|\\ \verb|B4: 4*c^2 = 2*b^2 |\foldedproof{2}\verb|;|\\ \verb|C3: 2*c^2 = b^2 |\foldedproof{3}\verb|;|\\ \verb|C4: b is even |\foldedproof{4}\verb|;|\\ \verb| thus contradiction |\foldedproof{5}\verb|;|\\ \verb|end;| \end{quote} Here the ellipsis symbols `$\ldots$' represent hidden subproofs of on average six lines each. The disadvantage of this approach is that the full formalization will not be `ordinary' Mizar. In a normal Mizar article subproofs occur much less often than here. A more natural way for Mizar to fold parts of a proof is to fold away steps. That way one gets: %\def\foldedline#1{$\clubsuit_{#1}$} \def\foldedline#1{$\,\ldots\,$} \begin{quote} \verb|theorem Th43: sqrt 2 is irrational| \\ \verb|proof| \\ \verb| assume sqrt 2 is rational;| \\ \verb| then consider a,b such that| \\ \verb| |\foldedline{1}\verb| and |\foldedline{2}\verb| and| \\ \verb|A1: a,b are_relative_prime by Def1;| \\ \verb| |\foldedline{3}\verb|; |\foldedline{4}\verb| |\foldedline{5}\verb|; then| \\ \verb|4_3_1: a^2 = 2*b^2 by B3,REAL_1:43;| \\ \verb| a^2 is even by 4_3_1,ABIAN:def 1;| \\ \verb| then| \\ \verb|A2: a is even by PYTHTRIP:2;| \\ \verb| then consider c such that| \\ \verb|A3: a = 2*c by ABIAN:def 1;| \\ \verb|B4: 4*c^2 |\foldedline{6}\verb| |\foldedline{7}\verb| .= 2*b^2 by A3,4_3_1,SQUARE_1:68;| \\ \verb| |\foldedline{8}\verb| |\foldedline{9}\verb|; then 2*c^2 = b^2 by REAL_1:9;| \\ \verb| |\foldedline{{10}}\verb|; then b is even by PYTHTRIP:2;| \\ \verb| |\foldedline{{11}}\verb|; |\foldedline{{12}}\verb|; |\foldedline{{13}}% \verb|; hence contradiction by B5,INT_2:17;| \\ \verb|end;| \end{quote} Note that this still is basically the same structure as the formal proof sketch, although it looks much `messier'. In this version the folded parts are all the same size, one line long: \def\foldedline#1{$\,\ldots_{#1}$} \begingroup \begin{eqnarray*} \mbox{\foldedline{\ 1}} & \equiv\, & \verb|B1: b <> 0| \\ \mbox{\foldedline{\ 2}} & \equiv\, & \verb|B2: sqrt 2 = a/b| \\ \mbox{\foldedline{\ 3}} & \equiv\, & \verb|B3: b^2 <> 0 by B1,SQUARE_1:73| \\ \mbox{\foldedline{\ 4}} & \equiv\, & \verb|2 = (a/b)^2 by B2,SQUARE_1:def 4| \\ \mbox{\foldedline{\ 5}} & \equiv\, & \verb| .= a^2/b^2 by SQUARE_1:69| \\ \mbox{\foldedline{\ 6}} & \equiv\, & \verb| = (2*2)*c^2| \\ \mbox{\foldedline{\ 7}} & \equiv\, & \verb| .= 2^2*c^2 by SQUARE_1:def 3| \\ \mbox{\foldedline{\ 8}} & \equiv\, & \verb|2*(2*c^2) = (2*2)*c^2 by AXIOMS:16| \\ \mbox{\foldedline{\ 9}} & \equiv\, & \verb| .= 2*b^2 by B4| \\ \mbox{\foldedline{{10}}} & \equiv\, & \verb|then b^2 is even by ABIAN:def 1| \\ \mbox{\foldedline{{11}}} & \equiv\, & \verb|then 2 divides a & 2 divides b by A2,Def2| \\ \mbox{\foldedline{{12}}} & \equiv\, & \verb|then B5: 2 divides a gcd b by INT_2:33| \\ \mbox{\foldedline{{13}}} & \equiv\, & \verb|a gcd b = 1 by A1,INT_2:def 4| \end{eqnarray*} \endgroup A third way of folding is to keep the proof the way it is, but to hide all labels and justifications: \begin{quote} \begin{verbatim} theorem Th43: sqrt 2 is irrational proof assume sqrt 2 is rational; consider a,b such that b <> 0 and sqrt 2 = a/b and a,b are_relative_prime; b^2 <> 0; 2 = (a/b)^2 .= a^2/b^2; a^2 = 2*b^2; a^2 is even; a is even; consider c such that a = 2*c; 4*c^2 = (2*2)*c^2 .= 2^2*c^2 .= 2*b^2; 2*(2*c^2) = (2*2)*c^2 .= 2*b^2; 2*c^2 = b^2; b^2 is even; b is even; 2 divides a & 2 divides b; 2 divides a gcd b; a gcd b = 1; thus contradiction; end; \end{verbatim} \end{quote} This is rather long, but it is much more readable than the formalization with the labels and justifications shown. \section{Another example}\label{geomath} We will now present a second example, taken from the linear algebra part of a textbook \cite{gal:01}. This textbook currently has not been published on paper yet, but it is available on the WWW. On p.~16, we find the lemma: \begin{quote} {\bf Lemma 2.1.} {\em Given a linearly independent family $(u_i)_{i\in I}$ of elements of a vector space $E$, if $v\in E$ is not a linear combination of $(u_i)_{i\in I}$, then the family $(u_i)_{i\in I}\cup_k (v)$ obtained by adding $v$ to the family $(u_i)_{i\in I}$ is linearly independent (where $k\not\in I$). } \medskip {\em Proof.} Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$, for any family $(\lambda_i)_{i\in I}$ of scalars in $K$. If $\mu\ne 0$, then $\mu$ has an inverse (because $K$ is a field), and thus we have $v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$, showing that $v$ is a linear combination of $(u_i)_{i\in I}$ and contradicting the hypothesis. Thus, $\mu = 0$. But then, we have $\sum_{i\in I} \lambda_i u_i = 0$, and since the family $(u_i)_{i\in I}$ is linearly independent, we have $\lambda_i = 0$ for all $i\in I$. $\hfill\Box$ \end{quote} The formal proof sketch that corresponds to this is: \begin{quote} \begin{verbatim} theorem Lem21: u is linearly-independent & not v in Lin(u) implies u \/ {v} is linearly-independent proof assume u is linearly-independent & not v in Lin(u); assume u \/ {v} is linearly-dependent; consider m being Element of K, l being Linear_Combination of u such that m*v + Sum(l) = 0.E; now assume m <> 0.K; v = -m"*Sum(l); v in Lin(u); thus contradiction; end; m = 0.K; Sum(l) = 0.E; Carrier(l) = {}; thus contradiction; end; \end{verbatim} \end{quote} To show the similarity between the two, here is the informal English version next to the formulas from the formal proof sketch: \begin{center} \begin{tabular}{rcl} Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$\rlap{,} &$\quad$& {\tt m*v + Sum(l) = 0.E}\\ for any family $(\lambda_i)_{i\in I}$ of scalars in $K$\rlap{.}\\ %&& {\tt l being }{\dots}\\ If $\mu\ne 0$\rlap{,} && {\tt m <> 0.K}\\ then $\mu$ has an inverse (because $K$ is a field)\rlap{,}\\ and thus we have $v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$\rlap{,} && {\tt v = -m"*Sum(l)}\\ showing that $v$ is a linear combination of $(u_i)_{i\in I}$ && {\tt v in Lin(u)}\\ and contradicting the hypothesis\rlap{.} && {\tt contradiction}\\ Thus, $\mu = 0$ && {\tt m = 0.K}\\ But then, we have $\sum_{i\in I} \lambda_i u_i = 0$\rlap{,} && {\tt Sum(l) = 0.E}\\ and since the family $(u_i)_{i\in I}$ is linearly independent\rlap{,}\\ we have $\lambda_i = 0$ for all $i\in I$\rlap{.} && {\tt Carrier(l) = }\verb|{}| \end{tabular} \end{center} Here is the full formalization that one gets by completing the formal proof sketch: \begin{quote} \verb|theorem|\\ \verb| u is linearly-independent & not v in Lin(u) implies|\\ \verb| u \/ {v} is linearly-independent|\\ \verb|proof|\\ \verb| assume|\\ \verb|A1: u is linearly-independent & not v in Lin(u);|\\ \verb| |\underbar{\tt{assume u {\char92}/ {\char123}v{\char125} is linearly-dependent;}}\\ \verb| then consider l' being Linear_Combination of u \/ {v}|\\ \verb| such that|\\ \verb|A2: Sum(l') = 0.E & Carrier(l') <> {} by VECTSP_7:def 1;|\\ \verb| consider m' being Linear_Combination of {v},|\\ \verb| l being Linear_Combination of u such that|\\ \verb|A3: l' = m' + l by Th2;|\\ \verb| set m = m'.v;|\\ \verb|A4: m*v + Sum(l) = Sum(m') + Sum(l) by VECTSP_6:43|\\ \verb| .= 0.E by A2,A3,VECTSP_6:77;|\\ \verb| now|\\ \verb| assume|\\ \verb|A5: m <> 0.K;|\\ \verb| m*v = -Sum(l) by A4,RLVECT_1:def 10;|\\ \verb| then v = m"*(-Sum(l)) by A5,VECTSP_1:67|\\ \verb| .= -m"*Sum(l) by VECTSP_1:69;|\\ \verb| then|\\ \verb|A6: v = (-m")*Sum(l) by VECTSP_1:68;|\\ \verb| Sum(l) in Lin(u) by VECTSP_7:12;|\\ \verb| |\underbar{\tt{then v in Lin(u) by A6,VECTSP\_4:29;}}\\ \verb| hence contradiction by A1;|\\ \verb| end;|\\ \verb| then|\\ \underbar{\tt{A7: m = 0.K;}}\\ \verb| Sum(l) = 0.E + Sum(l) by VECTSP_1:7|\\ \verb| .= 0.E by A4,A7,VECTSP_1:59;|\\ \verb| then|\\ \verb|A8: Carrier(l) = {} by A1,VECTSP_7:def 1;|\\ \verb| now|\\ \verb| let x be set;|\\ \verb|A9: Carrier(m') c= {v} by VECTSP_6:def 7;|\\ \verb| not v in Carrier(m') by A7,VECTSP_6:20;|\\ \verb| hence not x in Carrier(m') by A9,TARSKI:def 1;|\\ \verb| end;|\\ \verb| then Carrier(m') = {} by BOOLE:def 1;|\\ \verb| then Carrier(l) \/ Carrier(m') = {} by A8;|\\ \verb| then Carrier(l') c= {} by A3,VECTSP_6:51;|\\ \verb| hence contradiction by A2,BOOLE:30;|\\ \verb|end;| \end{quote} The steps that have been underlined in this proof can be omitted (as pointed out by the \verb|relinfer| tool). When one omits them, and then again extracts the formal proof sketch, one gets: \begin{quote} \verb|theorem Lem21:|\\ \verb| u is linearly-independent & not v in Lin(u) implies|\\ \verb| u \/ {v} is linearly-independent|\\ \verb|proof|\\ \verb| assume u is linearly-independent & not v in Lin(u);|\\ \verb| given l' being Linear_Combination of u \/ {v} such that|\\ \verb| Sum(l') = 0.E & Carrier(l') <> {};|\\ \verb| consider m' being Linear_Combination of {v},|\\ \verb| l being Linear_Combination of u such that|\\ \verb| l' = m' + l;|\\ \verb| set m = m'.v;|\\ \verb| m*v + Sum(l) = 0.E;|\\ \verb| now|\\ \verb| assume m <> 0.K;|\\ \verb| v = -m"*Sum(l);|\\ \verb| thus contradiction;|\\ \verb| end;|\\ \verb| Sum(l) = 0.E;|\\ \verb| Carrier(l) = {};|\\ \verb| thus contradiction;|\\ \verb|end;| \end{quote} This is clearly less readable than the first version of the formal proof sketch. When one does the experiment with HOL Light's \verb|MESON_TAC| for this example, one discovers that HOL Light is not even able to do the steps that Mizar can do. The reason for this is that the typing of the objects in this proof is quite involved, and it is too complicated to discover the necessary deductions to get the necessary typing judgments by first order proof search. The two steps in this example which are of the `algebraic problem' type, are: \begin{eqnarray*} \mu v + \sum\lambda = 0 \;\land\; \mu\ne 0 &\;\vdash\;& v = -\mu^{-1}\sum\lambda\\ \mu v + \sum\lambda = 0 \;\land\; \mu = 0 &\;\vdash\;& \sum\lambda = 0 \end{eqnarray*} These may seem trivial, but Mizar is not powerful enough to do either one of them in one step. Also, note that these are not algebraic problems about numbers, but about abstract entities like elements of an arbitrary field, vectors in an arbitrary vector space, and `linear combinations of vectors'. \section{Conclusion} \subsection{Discussion} We presented the notion of {\em formal proof sketch\/} and looked at some possibilities to use this to make a better interface for presentations of formalizations. The main things that one should consider are: \begin{itemize} \item The dual window approach from Section~\ref{dual}. \item The third variant of the folding interface from Section~\ref{folding}, where the labels and justifications can be hidden. \end{itemize} To get a `better' proof checker one should: \begin{itemize} \item Study algebraic decision procedures as discussed in Section~\ref{algebra}. \end{itemize} \subsection{Future work} We want to investigate the existing algebraic decision procedures (like for instance in the ICS system \cite{fil:owr:rue:sha:01}) to find out how well they can do the algebraic problems from Section~\ref{algebra}. \subsection{Acknowledgments} Thanks to Josef Urban for his translation of the proof obligations in a Mizar article to TPTP format. Thanks to Dan Synek for the example from Section~\ref{geomath}. Thanks to Henk Barendregt for encouraging remarks. %\bibliographystyle{plain} %\bibliography{frk} \begin{thebibliography}{1} \bibitem{fil:owr:rue:sha:01} Jean-Christophe Filli\^{a}tre, Sam Owre, Harald Rue\ss, and {N.} Shankar. \newblock {ICS:} integrated canonizer and solver. \newblock To be presented at {CAV'2001}, 2001. \bibitem{gal:01} Jean Gallier. \newblock {\em Basics of Algebra and Analysis For Computer Science}. \newblock University of Pennsylvania, 2001. \newblock Published at:\hfill\break URL: \verb||. \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:00} John Harrison. \newblock {\em The HOL Light manual (1.1)}, 2000. \newblock \hfill\break URL: \verb||. \bibitem{muz:93} M.~Muzalewski. \newblock {\em An Outline of PC Mizar}. \newblock Fondation Philippe le Hodey, Brussels, 1993. \newblock \hfill\break URL: \verb||. \bibitem{ned:01} Rob Nederpelt. \newblock {Weak Type Theory, a formal language for mathematics}. \newblock Draft version, July 2001. \bibitem{wie:99:1} F.~Wiedijk. \newblock {Mizar: An Impression}. \newblock \hfill\break URL: \verb||, 1999. \end{thebibliography} \appendix \section{The smallest first order problem from Section \ref{meson}} We will now show an example of the problems that we gave to \verb|MESON_TAC| in Section \ref{meson}. It is the smallest of these first order problems, which is step number 3 in the formal proof sketch. That problem is (where the variable \verb|a| has type \verb|Integer|): \begin{center} \begin{tabular}{c} \verb|a^2 is even|\\\noalign{\smallskip} \verb|for i being Integer holds i is even iff i^2 is even|\\\noalign{\smallskip} \hline\noalign{\smallskip} \verb|a is even|\\ \end{tabular} \end{center} The corresponding problem that we gave to \verb|MESON_TAC| looks much more complicated: \begin{flushleft}\footnotesize \verb|v1_abian (k5_square_1 c1) /\|\\ \verb|(!U:V. v1_int_1 U|\\ \verb| ==> ~(v1_abian U /\ ~v1_abian (k5_square_1 U)) /\|\\ \verb| ~(v1_abian (k5_square_1 U) /\ ~v1_abian U)) /\|\\ \verb|v1_int_1 c1 /\|\\ \verb|v1_int_1 c2 /\|\\ \verb|(!U. m1_subset_1 U k1_arytm ==> m1_subset_1 (k5_square_1 U) k1_arytm) /\|\toolong\\ \verb|(!U. m1_subset_1 U k5_ordinal2 ==> m1_subset_1 (k5_square_1 U) k5_ordinal2) /\|\toolong\\ \verb|(!U. v1_int_1 U ==> m1_subset_1 (k5_square_1 U) k5_ordinal2) /\|\\ \verb|(!U. v1_int_1 U ==> v1_arytm U) /\|\\ \verb|(!U V W.|\\ \verb| (~v1_subset_1 U /\ ~v1_subset_1 V /\ m1_subset_1 V (k1_zfmisc_1 U)) /\|\toolong\\ \verb| m1_subset_1 W V|\\ \verb| ==> m1_subset_1 W U) /\|\\ \verb|m1_subset_1 k5_ordinal2 (k1_zfmisc_1 k1_arytm) /\|\\ \verb|(!U. m1_subset_1 U k5_ordinal2|\\ \verb| ==> v1_ordinal1 U /\|\\ \verb| v2_ordinal1 U /\|\\ \verb| v3_ordinal1 U /\|\\ \verb| v4_ordinal2 U /\|\\ \verb| v1_arytm U /\|\\ \verb| v1_int_1 U) /\|\\ \verb|(!U. m1_subset_1 U k1_arytm ==> v1_arytm U) /\|\\ \verb|(!U. v1_arytm U ==> v1_arytm (k5_square_1 U)) /\|\\ \verb|~v1_subset_1 k1_arytm /\|\\ \verb|~v1_subset_1 k5_ordinal2 /\|\\ \verb|(!U. v4_ordinal2 U ==> v1_int_1 U) /\|\\ \verb|(!U. v4_ordinal2 U ==> v1_arytm U) /\|\\ \verb|(!U V. r2_hidden U V = m1_subset_1 U V /\ ~v1_subset_1 V) /\|\\ \verb|(!U V. r1_tarski U V = m1_subset_1 U (k1_zfmisc_1 V)) /\|\\ \verb|(!U V. v1_subset_1 U /\ ~(U = V) ==> ~v1_subset_1 V) /\|\\ \verb|(!U. r1_tarski U U) /\|\\ \verb|(!U. v3_ordinal1 U ==> r1_tarski U U) /\|\\ \verb|(!U V. v3_ordinal1 U /\ v3_ordinal1 V ==> r1_tarski U V \/ r1_tarski V U) /\|\toolong\\ \verb|(!U V. r2_hidden U V ==> ~r2_hidden V U) /\|\\ \verb|(!U V W.|\\ \verb| r2_hidden U V /\ m1_subset_1 V (k1_zfmisc_1 W)|\\ \verb| ==> m1_subset_1 U W /\ ~v1_subset_1 W)|\\ \verb|==> v1_abian c1| \end{flushleft} The reason for this is that we use \verb|MESON_TAC| as an untyped prover (the HOL type system is not powerful enough to accommodate the Mizar type system), so all relevant typing judgments have to be given as first order sentences. The syntax that is used here does not use Mizar notation, but gives each `constructor' with a code. These codes translate back to the original Mizar notation according to the following table: \begin{center} \begin{tabular}{lcl} \verb|k1_zfmisc_1| &$\qquad$& \verb|bool| \\ \verb|k5_ordinal2| && \verb|NAT| \\ \verb|k1_arytm| && \verb|REAL| \\ \verb|k5_square_1| && \verb|^2| \\ \verb|r2_hidden| && \verb|in| \\ \verb|r1_tarski| && \verb|c=| \\ \verb|m1_subset_1| && \verb|Element| \\ \verb|v1_subset_1| && \verb|empty| \\ \verb|v1_ordinal1| && \verb|epsilon-transitive| \\ \verb|v2_ordinal1| && \verb|epsilon-connected| \\ \verb|v3_ordinal1| && \verb|ordinal| \\ \verb|v4_ordinal2| && \verb|natural| \\ \verb|v1_int_1| && \verb|integer| \\ \verb|v1_arytm| && \verb|real| \\ \verb|v1_abian| && \verb|even| \end{tabular} \end{center} We now transform the HOL problem back to Mizar using this translation. Note the following Mizar type equivalences: \begin{eqnarray*} \verb|Nat| &\equiv& \verb|Element of NAT|\\ \verb|Integer| &\equiv& \verb|integer set|\\ \verb|Real| &\equiv& \verb|Element of REAL|\\ \verb|Subset of X| &\equiv& \verb|Element of bool X| \end{eqnarray*} The problem that we gave to \verb|MESON_TAC| is in Mizar notation: \begin{center}\footnotesize \begin{tabular}{c} \verb|a^2 is even|\\\noalign{\medskip} \verb|for i being integer set holds i is even iff i^2 is even|\\\noalign{\medskip} \verb|a is integer|\\\noalign{\medskip} \verb|b is integer|\\\noalign{\medskip} \verb|for x being Element of REAL holds x^2 is Element of REAL|\\\noalign{\medskip} \verb|for n being Element of NAT holds n^2 is Element of NAT|\\\noalign{\medskip} \verb|for a being integer set holds a^2 is Element of NAT|\\\noalign{\medskip} \verb|for IT being integer set holds IT is real|\\\noalign{\medskip} \verb|for D being non empty set, X being non empty Element of bool D,|\\ \verb|IT being Element of X holds IT is Element of D|\\\noalign{\medskip} \verb|NAT is Element of bool REAL|\\\noalign{\medskip} \verb|for IT being Element of NAT holds IT is epsilon-transitive|\\ \verb|epsilon-connected ordinal natural real integer|\\\noalign{\medskip} \verb|for IT being Element of REAL holds IT is real|\\\noalign{\medskip} \verb|for x being real set holds x^2 is real|\\\noalign{\medskip} \verb|REAL is non empty|\\\noalign{\medskip} \verb|NAT is non empty|\\\noalign{\medskip} \verb|for IT being natural set holds IT is integer|\\\noalign{\medskip} \verb|for IT being natural set holds IT is real|\\\noalign{\medskip} \verb|for U,V being set holds U in V iff (U is Element of V & V is non empty)|\\\noalign{\medskip} \verb|for U,V being set holds U c= V iff U is Element of bool V|\\\noalign{\medskip} \verb|for U,V being set st U is empty & U <> V holds V is non empty|\\\noalign{\medskip} \verb|for U being set holds U c= U|\\\noalign{\medskip} \verb|for U being ordinal set holds U c= U|\\\noalign{\medskip} \verb|for U being ordinal set, V being ordinal set holds U c= V or V c= U|\\\noalign{\medskip} \verb|for U being set, V being set st U in V holds not V in U|\\\noalign{\medskip} \verb|for U,V,W being set st U in V & V is Element of bool W holds|\\ \verb|U is Element of W & W is non empty|\\\noalign{\medskip} \hline\noalign{\medskip} \verb|a is even| \end{tabular} \end{center} \end{document}