\documentclass[a4]{seminar}
\usepackage{advi}
%\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xypic}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large formal proof sketches and MoWGLI}

Freek Wiedijk \\
University of Nijmegen

Proof Tools Day 2003 \\
CWI \\
Amsterdam

2003 04 25, 14:30
\end{slide}

\begin{slide}
\sectiontitle{formal proof sketches}
\slidetitle{\textbf{problem 1:} what to do with formal proofs?}
end product of a formalization project: tar file of scripts
\adviwait

what people look at: the statements of the lemmas \\
\adviwait
\red{proof scripts are `write only'}
\adviwait
\bigskip

many projects: \green{presenting formal proofs in natural language}
\adviwait
\medskip

MoWGLI project (Bologna, INRIA, Saarbr\"ucken, Berlin, Nijmegen)
\begin{center}
\textbf{Coq script} $\stackrel{\sf Coq\,}{\relbar\joinrel\longrightarrow}$ Coq XML $\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ OMDoc XML \advirecord{HTML}{$\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ \textbf{English} HTML}\adviplay{HTML}
\end{center}
\adviwait
%\adviplay[slidegray]{HTML}
%\adviwait
\medskip

generated text should become better \\
currently: rather verbose
%\adviwait
%(folding of subproofs doesn't help much)
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{problem 2:} only formalization of the interesting parts?}
Peter Aczel (at TYPES 2002 meeting): \\
getting mathematicians interested in formalization
%\adviwait

\red{light weight formalization} \\
don't prove everything: use axioms liberally
\adviwait
\bigskip

Leslie Lamport: \green{\textbf{How to Write a Proof}} (1993) \\
recursive clarification process: \red{hierarchical proofs} \\
\adviwait
not formal
\adviwait
\medskip

IMP project (Paul Cairns \& Jeremy Gow, London): implementation \\
interactive course notes: \green{Elements of Euclidean and Metric Topology}$\hspace{-2em}$ %\\
%\adviwait
%used in actual topology courses

experience: structure not easily understood
\vfill
\end{slide}

\begin{slide}
\slidetitle{an informal proof}
%\green{prover comparison}: proofs of \red{irrationality of $\sqrt{2}$} \\
%%\adviwait
%\textbf{HOL Light}: 29 lines, \textbf{Mizar}: 44 lines, \textbf{Coq}: 68 lines, \textbf{PVS}: 77 lines, \textbf{Isabelle}: 114 lines
%%\adviwait
%%($+$ ten more systems)
%\adviwait
%\medskip
%
Hardy \& Wright, \green{An Introduction to the Theory of Numbers}%: \textbf{7 lines}
\adviwait
\medskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}
\begin{center}
\setlength{\fboxsep}{.5em}
$\hspace{-2em}$\framebox{\hspace{.1em}\parbox{\linewidth}{
\textbf{Theorem 43 (Pythagoras' theorem).} {$\sqrt{2}$ is irrational.}
\medskip

\rightskip=0pt
The traditional proof ascribed to Pythagoras runs
as follows.  If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{\textsf{(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$%
\smallskip
}\hspace{.3em}}$\hspace{-2em}$
\end{center}
\end{quote}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{`formal proof sketch'}
\green{exactly same reasoning, using Mizar syntax}
\medskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}\small
\advirecord{a1}{\textbf{theorem} Th43: sqrt 2 is irrational} \\
%$\,$:: \textbf{Pythagoras' theorem}}$\hspace{-1em}$ \\
\advirecord{a2}{\textbf{proof}} \\
\advirecord{a3}{\quadskip \textbf{assume} sqrt 2 is rational\textbf{;}} \\
\advirecord{a4}{\quadskip \textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}} \\
\advirecord{a5}{4\_3\_1: a\char`^2 = 2$\,*\,$b\char`^2 \textbf{and}} \\
\advirecord{a6}{\quadskip\quadskip a,b are\_relative\_prime\textbf{;}} \\
\advirecord{a7}{\quadskip a\char`^2 is even\textbf{;}} \\
\advirecord{a8}{\quadskip a is even\textbf{;}} \\
\advirecord{a9}{\quadskip \textbf{consider} c \textbf{such that} a = 2$\,*\,$c\textbf{;}} \\
\advirecord{a10}{\quadskip 4$\,*\,$c\char`^2 = 2$\,*\,$b\char`^2\textbf{;}} \\
\advirecord{a11}{\quadskip 2$\,*\,$c\char`^2 = b\char`^2\textbf{;}} \\
\advirecord{a12}{\quadskip b is even\textbf{;}} \\
\advirecord{a13}{\quadskip \textbf{thus} contradiction\textbf{;}} \\
\advirecord{a14}{\textbf{end;}}
\end{quote}
\adviplay{a1}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviplay{a5}
\adviplay{a6}
\adviplay{a7}
\adviplay{a8}
\adviplay{a9}
\adviplay{a10}
\adviplay{a11}
\adviplay{a12}
\adviplay{a13}
\adviplay{a14}
\vss
}
\adviwait
\vbox to 0pt{
\vspace{-2.2\bigskipamount}
\begin{quote}
\rightskip=0pt
\advirecord{b1}{\textbf{theorem} Th43: {sqrt 2 is irrational} $\,$:: \textbf{Pythagoras' theorem}}
\medskip

\advirecord{b2}{\textbf{proof}$\,$} \advirecord{b3}{assume sqrt 2
is rational;} \advirecord{b4}{consider $a,b$ such that}
\advirecord{b5}{$$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$
and} \advirecord{b6}{$a,b$ are\_relative\_prime;} \advirecord{b7}{$a\mathbin{\hat{}}2$ is even;}
\advirecord{b8}{$a$ is even;} \advirecord{b9}{consider $c$ such that $a = 2\mathbin{*}c$;} \advirecord{b10}{$4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$;} \advirecord{b11}{$2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$;} \advirecord{b12}{$b$ is
even;} \advirecord{b13}{thus contradiction;} \hfill \advirecord{b14}{end;}
\end{quote}
\adviplay[white]{a1}\adviplay{b1}\adviwait[.8]
\adviplay[white]{a2}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a3}\adviplay{b3}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a4}\adviplay{b4}\adviwait[.8]
\adviplay[white]{a5}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a6}\adviplay{b6}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a7}\adviplay{b7}\adviwait[.8]
\adviplay[white]{a8}\adviplay{b8}\adviwait[.8]
\adviplay[white]{a9}\adviplay{b9}\adviwait[.8]
\adviplay[white]{a10}\adviplay{b10}\adviwait[.8]
\adviplay[white]{a11}\adviplay{b11}\adviwait[.8]
\adviplay[white]{a12}\adviplay{b12}\adviwait[.8]
\adviplay[white]{a13}\adviplay{b13}\adviwait[.8]
\adviplay[white]{a14}\adviplay{b14}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{full formalization}
\green{filling out the formal proof sketch to a checkable Mizar text}
\medskip

\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c1}{\textbf{theorem} Th43: sqrt 2 is irrational}\\
\advirecord{c2}{\textbf{proof}}\\
\advirecord{c3}{\quad \textbf{assume} sqrt 2 is rational\textbf{;}}\\
\advirecord{c4}{\quad \textbf{then} }\advirecord{c5}{\textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}}\\
\advirecord{c6a}{A1: }\advirecord{c6b}{b {\tiny \raise.8pt\hbox{$<>$}} 0 \textbf{and}}\\
\advirecord{c7a}{A2: }\advirecord{c7b}{sqrt 2 = a/b \textbf{and}}\\
\advirecord{c8}{A3: }\advirecord{c9}{a,{\tiny $\,$}b are\_relative\_prime}\advirecord{c10a}{ \textbf{by} Def1}\advirecord{c10b}{\textbf{;}}\\
\advirecord{c11a}{A4: }\advirecord{c11b}{b\^{}2 {\tiny \raise.8pt\hbox{$<>$}} 0}\advirecord{c11c}{ \textbf{by} A1,{\tiny $\,$}{\tiny SQUARE\_}1:73}\advirecord{c11d}{\textbf{;}}\\
\advirecord{c12a}{\quad 2 = (a/b)\^{}2}\advirecord{c12b}{ \textbf{by} A2,{\tiny $\,$}{\tiny SQUARE\_}1:def 4}\\
\advirecord{c13a}{\qquad .= a\^{}2/b\^{}2}\advirecord{c13b}{ \textbf{by} {\tiny SQUARE\_}1:69}\advirecord{c13c}{\textbf{;}}\\
\advirecord{c14}{\quad \textbf{then}}\\
\advirecord{c15}{4\_3\_1: a\^{}2 = 2$\,*\,$b\^{}2}\advirecord{c16}{ \textbf{by} A4,{\tiny $\,$}{\tiny REAL\_}1:43}\advirecord{c17}{\textbf{;}}\\
\advirecord{c18}{\quad a\^{}2 is even}\advirecord{c19}{ \textbf{by} 4\_3\_1,{\tiny $\,$}{\tiny ABIAN}:def 1}\advirecord{c20}{\textbf{;}}\\
\advirecord{c21}{\quad \textbf{then}}\\
\advirecord{c22}{A5: }\advirecord{c23}{a is even}\advirecord{c24}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c25}{\textbf{;}}\\
\green{:: \textbf{continue in next column}}
\end{flushleft}
}\hfill\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c26}{\quad \textbf{then} }\advirecord{c27}{\textbf{consider} c \textbf{such that}} \\
\advirecord{c28}{A6: }\advirecord{c29}{a = 2$\,*\,$c}\advirecord{c30}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c31}{\textbf{;}} \\
\advirecord{c32}{A7: }\advirecord{c33}{4$\,*\,$c\^{}2 =}\advirecord{c34}{ (2$\,*\,$2)$\,*\,$c\^{}2}\\
\advirecord{c35a}{\qquad .= 2\^{}2$\,*\,$c\^{}2}\advirecord{c35b}{ \textbf{by} {\tiny SQUARE\_}1:def 3}\\
\advirecord{c36}{\qquad .= }\advirecord{c37}{2$\,*\,$b\^{}2}\advirecord{c38}{ \textbf{by} A6,{\tiny $\,$}4\_3\_1,{\tiny $\,$}{\tiny SQUARE\_}1:68}\advirecord{c39}{\textbf{;}}\\
\advirecord{c40a}{\quad 2$\,*\,$(2$\,*\,$c\^{}2) = (2$\,*\,$2)$\,*\,$c\^{}2}\advirecord{c40b}{ \textbf{by} {\tiny AXIOMS}:16}\\
\advirecord{c41a}{\qquad .= 2$\,*\,$b\^{}2}\advirecord{c41b}{ \textbf{by} A7}\advirecord{c41c}{\textbf{;}}\\
\advirecord{c42}{\quad \textbf{then} }\advirecord{c43}{2$\,*\,$c\^{}2 = b\^{}2}\advirecord{c44}{ \textbf{by} {\tiny REAL\_}1:9}\advirecord{c45}{\textbf{;}}\\
\advirecord{c46a}{\quad \textbf{then} }\advirecord{c46b}{b\^{}2 is even}\advirecord{c46c}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c46d}{\textbf{;}}\\
\advirecord{c47}{\quad \textbf{then} }\advirecord{c48}{b is even}\advirecord{c49}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c50}{\textbf{;}}\\
\advirecord{c51a}{\quad \textbf{then} }\advirecord{c51b}{2 divides a \& 2 divides b}\advirecord{c51c}{ \textbf{by} A5,{\tiny $\,$}Def2}\advirecord{c51d}{\textbf{;}}\\
\advirecord{c52}{\quad \textbf{then}}\\
\advirecord{c53a}{A8: }\advirecord{c53b}{2 divides a gcd b}\advirecord{c53c}{ \textbf{by} {\tiny INT\_}2:33}\advirecord{c53d}{\textbf{;}}\\
\advirecord{c54a}{\quad a gcd b = 1}\advirecord{c54b}{ \textbf{by} A3,{\tiny $\,$}{\tiny INT\_}2:def 4}\advirecord{c54c}{\textbf{;}}\\
\advirecord{c55}{\quad \textbf{hence} contradiction}\advirecord{c56}{ \textbf{by} A8,{\tiny $\,$}{\tiny INT\_}2:17}\advirecord{c57}{\textbf{;}}\\
\advirecord{c58}{\textbf{end;}}
\end{flushleft}
}
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay{c5}
\adviplay{c9}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c23}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviplay{c33}
\adviplay{c37}
\adviplay{c39}
\adviplay{c43}
\adviplay{c45}
\adviplay{c48}
\adviplay{c50}
\adviplay{c55}
\adviplay{c57}
\adviplay{c58}
\adviwait
\adviplay[slideblue]{c6b}
\adviplay[slideblue]{c7b}
\adviplay[slideblue]{c10b}
\adviplay[slideblue]{c11b}
\adviplay[slideblue]{c11d}
\adviplay[slideblue]{c12a}
\adviplay[slideblue]{c13a}
\adviplay[slideblue]{c13c}
\adviplay[slideblue]{c34}
\adviplay[slideblue]{c35a}
\adviplay[slideblue]{c36}
\adviplay[slideblue]{c40a}
\adviplay[slideblue]{c41a}
\adviplay[slideblue]{c41c}
\adviplay[slideblue]{c46b}
\adviplay[slideblue]{c46d}
\adviplay[slideblue]{c51b}
\adviplay[slideblue]{c51d}
\adviplay[slideblue]{c53b}
\adviplay[slideblue]{c53d}
\adviplay[slideblue]{c54a}
\adviplay[slideblue]{c54c}
\adviwait
\adviplay[slidered]{c4}
\adviplay[slidered]{c14}
\adviplay[slidered]{c21}
\adviplay[slidered]{c26}
\adviplay[slidered]{c42}
\adviplay[slidered]{c46a}
\adviplay[slidered]{c47}
\adviplay[slidered]{c51a}
\adviplay[slidered]{c52}
\adviwait
\adviplay[slidered]{c6a}
\adviplay[slidered]{c7a}
\adviplay[slidered]{c8}
\adviplay[slidered]{c11a}
\adviplay[slidered]{c22}
\adviplay[slidered]{c28}
\adviplay[slidered]{c32}
\adviplay[slidered]{c53a}
\adviwait
\adviplay[slidered]{c10a}
\adviplay[slidered]{c11c}
\adviplay[slidered]{c12b}
\adviplay[slidered]{c13b}
\adviplay[slidered]{c16}
\adviplay[slidered]{c19}
\adviplay[slidered]{c24}
\adviplay[slidered]{c30}
\adviplay[slidered]{c35b}
\adviplay[slidered]{c38}
\adviplay[slidered]{c40b}
\adviplay[slidered]{c41b}
\adviplay[slidered]{c44}
\adviplay[slidered]{c46c}
\adviplay[slidered]{c49}
\adviplay[slidered]{c51c}
\adviplay[slidered]{c53c}
\adviplay[slidered]{c54b}
\adviplay[slidered]{c56}
\adviwait
\adviplay{c6b}
\adviplay{c7b}
\adviplay{c10b}
\adviplay{c11b}
\adviplay{c11d}
\adviplay{c12a}
\adviplay{c13a}
\adviplay{c13c}
\adviplay{c34}
\adviplay{c35a}
\adviplay{c36}
\adviplay{c40a}
\adviplay{c41a}
\adviplay{c41c}
\adviplay{c46b}
\adviplay{c46d}
\adviplay{c51b}
\adviplay{c51d}
\adviplay{c53b}
\adviplay{c53d}
\adviplay{c54a}
\adviplay{c54c}
\adviplay{c4}
\adviplay{c14}
\adviplay{c21}
\adviplay{c26}
\adviplay{c42}
\adviplay{c46a}
\adviplay{c47}
\adviplay{c51a}
\adviplay{c52}
\adviplay{c6a}
\adviplay{c7a}
\adviplay{c8}
\adviplay{c11a}
\adviplay{c22}
\adviplay{c28}
\adviplay{c32}
\adviplay{c53a}
\adviplay{c10a}
\adviplay{c11c}
\adviplay{c12b}
\adviplay{c13b}
\adviplay{c16}
\adviplay{c19}
\adviplay{c24}
\adviplay{c30}
\adviplay{c35b}
\adviplay{c38}
\adviplay{c40b}
\adviplay{c41b}
\adviplay{c44}
\adviplay{c46c}
\adviplay{c49}
\adviplay{c51c}
\adviplay{c53c}
\adviplay{c54b}
\adviplay{c56}
\vfill
\end{slide}

\begin{slide}
\slidetitle{incomplete but completable proofs}
formal proof sketch: \textbf{only} `inference errors' \\
\adviwait
completable into a checkable proof by adding:
\begin{itemize}
\item[$\bullet$]
\textbf{steps} %\\
%\advirecord{e1}{not only subproofs, but also steps in-between!} %\\
%\advirecord{e2}{problems for automated theorem provers} \advirecord{e3}{(Josef Urban's MPTP)}
\item[$\bullet$]
\textbf{labels/references} %\\
%\advirecord{e4}{informal proofs also have some references, but!}
\end{itemize}
\adviwait
%\adviplay{e1}
%\adviwait
%\adviplay{e2}
%\adviwait
%\adviplay{e3}
%\adviwait
%\adviplay{e4}
%\adviwait
\medskip

\red{formal} proof sketches \\
\adviwait
correctness: semi-decidable
\adviwait
\bigskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{center}
\begin{picture}(300,50)
\put(40,24){\makebox(0,0){no proofs}}
\put(40,10){\line(0,1){8}}
\advirecord{f1a}{\put(260,10){\line(0,1){8}}}%
\advirecord{f2a}{\put(40,14){\line(1,0){220}}}%
\advirecord{f3a}{\put(260,24){\makebox(0,0){full proofs}}}%
\put(150,0){\makebox(0,0){\blue{formal proof sketch spectrum}}}
\advirecord{f1b}{\put(160,10){\line(0,1){8}}}%
\advirecord{f2b}{\put(40,14){\line(1,0){120}}}%
\advirecord{f3b}{\put(160,24){\makebox(0,0){full proofs}}}%
\advirecord{fx1}{\green{\put(120,31){\vector(0,-1){17}}}}
\advirecord{fx2}{\put(120,49){\makebox(0,0){\green{`human level'}}}}
\advirecord{fx3}{\put(120,38){\makebox(0,0){\green{formal proof sketches}}}}
\end{picture}
\end{center}
\adviplay{f1a}\adviplay{f2a}\adviplay{f3a}
\adviwait
\adviplay{fx1}\adviplay{fx2}\adviplay{fx3}
\adviwait
\adviplay[white]{f1a}\adviplay[white]{f2a}\adviplay[white]{f3a}
\adviplay{f1b}\adviplay{f2b}\adviplay{f3b}
\vss}
\vfill
\end{slide}

\begin{slide}
\slidetitle{declarative proof style}
formal proof sketches (in this talk): \green{Mizar system}
\adviwait
\medskip

some reinventions of Mizar proof style:
\begin{itemize}
\item[$\bullet$]
Markus Wenzel's Isar language for the Isabelle system
\item[$\bullet$]
Henk Barendregt's `math mode' plans for the Coq system
\end{itemize}
\adviwait
\medskip

\red{forward reasoning} \\
\notion{label}\textbf{:} \notion{statement} \textbf{by} \notion{references}\textbf{;}
\adviwait
%\medskip

\red{natural deduction}
\begin{tabular}{lcl}
$\to$-introduction &$\,\to\,$& \textbf{assume} \notion{proposition}\textbf{;} \vspace{-\smallskipamount}\\
$\exists$-elimination &$\,\to\,$& \textbf{consider} \notion{variable} \textbf{such that} \notion{proposition}\textbf{;} \vspace{-\smallskipamount}\\
etc.
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch grammar}
\vbox to 0pt{
\vspace{-\bigskipamount}
\vspace{-\smallskipamount}
\begin{tabular}{rcl}
statement &=& proposition \advirecord{d1}{justification} \\
% &$|$& \advirecord{d2}{$[\,$label \textbf{:}$\,]$} term \textbf{=} term \advirecord{d3}{justification} \vspace{-\smallskipamount}\\
% && \quad $\{$\textbf{.=} term \advirecord{d4}{justification}$\}$ \vspace{-\smallskipamount}\\
proposition &=& \advirecord{d5}{$[\,$label \textbf{:}$\,]$} formula \\
% formula &=& {\dots} $\;\;|\;\;$ \textbf{thesis} \vspace{-\smallskipamount}\\
justification &=& \advirecord{d6a}{$[\,$\textbf{by} label $\{$\textbf{,} label$\}\,]$} \vspace{-\smallskipamount}\\
 &\advirecord{d6b}{$|$}& \textbf{proof} $\{$step \textbf{;}$\}$ $[\,$cases$\,]$ \textbf{end} \\
step &=& \advirecord{d7}{$[\,$\textbf{then}$\,]$} statement
% $\;\;|\;\;$ \textbf{set} variable \textbf{=} term
 \vspace{-\smallskipamount}\\
 &$|$& \textbf{assume} proposition
 \vspace{-\smallskipamount}\\
 &$|$& \textbf{let} variable $\{$\textbf{,} variable$\}$ \vspace{-\smallskipamount}\\
 &$|$& \advirecord{d8a}{$($}\textbf{thus} \advirecord{d8b}{$|$ \textbf{hence}$)$} statement \vspace{-\smallskipamount}\\
 &$|$& \advirecord{d9}{$[\,$\textbf{then}$\,]$} \textbf{consider} variable $\{$\textbf{,} variable$\}$ \vspace{-\smallskipamount}\\
 && \quad \textbf{such} \textbf{that} proposition \advirecord{d10}{justification} \vspace{-\smallskipamount}\\
 &$|$& \textbf{take} term $\{$\textbf{,} term$\}$ \\
cases &=& \textbf{per} \textbf{cases} \advirecord{d11}{justification} \textbf{;} \vspace{-\smallskipamount} \\
 && \quad $\big\{$\textbf{suppose} proposition \textbf{;} $\{$step \textbf{;}$\}\big\}\hspace{-3em}$
\end{tabular}
\adviplay{d1}
\adviplay{d2}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviplay{d6a}
\adviplay{d6b}
\adviplay{d7}
\adviplay{d8a}
\adviplay{d8b}
\adviplay{d9}
\adviplay{d10}
\adviplay{d11}
\adviwait
\adviplay[slidegray]{d1}
\adviplay[slidegray]{d2}
\adviplay[slidegray]{d3}
\adviplay[slidegray]{d4}
\adviplay[slidegray]{d5}
\adviplay[slidegray]{d6a}
\adviplay[slidegray]{d6b}
\adviplay[slidegray]{d7}
\adviplay[slidegray]{d8a}
\adviplay[slidegray]{d8b}
\adviplay[slidegray]{d9}
\adviplay[slidegray]{d10}
\adviplay[slidegray]{d11}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{generating formal proof sketches?}
\green{full Mizar formalization $\relbar\joinrel\longrightarrow$ formal proof sketch}
\adviwait
\medskip

systematic procedure (works surprisingly well)
\adviwait
\begin{itemize}
\item[$\bullet$]
remove all labels/references
\adviwait
\item[$\bullet$]
remove `in-between' steps % (and maybe some sub-proofs)
\end{itemize}
\adviwait
\medskip

but how to locate the \red{important steps} in a proof?
\adviwait
\begin{itemize}
\item[$\bullet$]
\textbf{user tagging} \\
\adviwait
no support for this in the Mizar language \adviwait (yet)
\adviwait
\item[$\bullet$]
\textbf{heuristics} \\
\adviwait
%no good heuristics known to me \\
formal proof sketches can't be generated automatically \adviwait (yet)
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof development cycle}
% \xymatrix{
% \mbox{informal text}\adviwait\ar@{->}[r] & \mbox{formal proof sketch}\adviwait\ar@(dr,ul)@{->}[rrd] &&\\
% & \mbox{\advirecord{g}{formal proof sketch}} && \mbox{full formalization}\adviwait\ar@{-}[ll]\adviplay{g}
% }
\vspace{-\bigskipamount}
$$\xymatrix@=1.5em{
\mbox{informal text}\adviwait\ar@{->}[d] \\
\mbox{formal proof sketch}\adviwait\ar@(dr,ul)@{->}[rd] & \mbox{\advirecord{g}{formal proof sketch}} \\
& \mbox{full formalization}\adviwait\ar@{.}[u]\adviplay{g}
}$$
\adviwait

\blue{\textbf{comparing sizes:}}
\begin{center}
%formal proof sketch $\;\ll\;$ full formalization \advirecord{h}{${\mathop{\;\ll\;}\limits_{\sf\green{in\;practice}}}$ generated language}$\hspace{-1em}$
formal proof sketch $\;\ll\;$ full formalization $\;\ll\;$ generated language
\end{center}
%\adviwait
%\adviplay{h}
\adviwait
\medskip

human attention span is important \\
%\adviwait
\red{presentation should be much smaller than the formalization} %\\
%\adviwait
%(`more explanation' is not the same as `easier to understand'!)
%\adviwait

%proof presentation: should be \green{road map to the full formal proof} \\

\adviwait
\bigskip
(\blue{folding sub-proofs}: doesn't help!)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{MoWGLI}
\slidetitle{`Mathematics on the Web, Get it by Logic and Interfaces'}
\red{project goal: more intelligent math documents}

\advirecord{x1}{formalizations $\to$ more than tar file of scripts} \\
\advirecord{x2}{publishing $\to$ not only for print/screen}
\adviwait
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{formalizations} (Coq) \\
\advirecord{w1}{Bologna: HELM project} \\
\advirecord{w2}{Sophia/Paris: INRIA, Trusted Logic} \\
\advirecord{w3}{Nijmegen: FTA project} % ($\to$ C-CoRN)}

\item[$\bullet$]
\textbf{math/physics publishing} \\
\advirecord{w4}{Berlin: Living Reviews in Relativity, Zentrallblatt} \\
%
%\item[$\bullet$]
%\textbf{interactive textbooks} \\
\advirecord{w5}{Saarbr\"ucken: ActiveMath}
\end{itemize}
\adviwait
\adviplay{w1}\adviplay{w2}\adviplay{w3}
%\adviwait
\adviplay[slidegreen]{x1}
\adviwait
\adviplay{w4}\adviplay{w5}
%\adviwait
\adviplay[slidegreen]{x2}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\green{proof: 5 lines of Coq}
\begin{quote}
\red{\textbf{Definition}} ge [n,m:\blue{nat}] :\ Prop := \\
\quadskip ({\small EX} x:\blue{nat} $|$ n = (\blue{plus} m x)).
\end{quote}

\begin{quote}
\red{\textbf{Lemma}} ge\_trans :\ (n,m,p:\blue{nat})(\blue{ge} n m)$\to$(\blue{ge} m p)$\to$(\blue{ge} n p). \\
\red{\textbf{Proof}}. \\
\enskipp Unfold ge.\ Intros n m p H H0. \\
\enskipp Elim H.\ Clear H.\ Intros x H1. \\
\enskipp Elim H0.\ Clear H0.\ Intros x0 H2. \\
\enskipp Exists (\blue{plus} x0 x). \\
\enskipp Rewrite \blue{plus\_assoc\_l}.\ Rewrite $\leftarrow$ H2.\ Auto. \\
\red{\textbf{Qed}}.
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{MoWGLI presentation}
\green{proof: 24 lines of HTML (almost 5 times as many lines)}
\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}\hbox{}\tiny
\red{assume} n\red{:} $\,$\blue{nat} \\
\red{assume} m\red{:} $\,$\blue{nat} \\
\red{assume} p\red{:} $\,$\blue{nat} \\
\red{suppose} H\red{:} $\,$(n\blue{$\ge$}m) \\
\red{suppose} $\,$H 0 \red{:} $\,$(m\blue{$\ge$}p) \\
\enskipp \red{consider} H \\
\enskipp \red{we proved} (n\blue{$\ge$}m) \\
\enskipp \red{that is equivalent to} \blue{$\exists$}z:\blue{nat}.(n\blue{=}(m\blue{+}z)) \\
\enskipp \red{there exists} x\red{:} $\,$\blue{nat} $\,$\red{such that} \\
\enskipp \red{(} H 1 \red{)} $\,$(n\blue{=}(m\blue{+}x)) \\
\enskipp \red{consider} $\,$H 0 \\
\enskipp \red{we proved} (m\blue{$\ge$}p) \\
\enskipp \red{that is equivalent to} \blue{$\exists$}z:\blue{nat}.(m\blue{=}(p\blue{+}z)) \\
\enskipp \red{there exists} $\,$x 0 \red{:} $\,$\blue{nat} $\,$\red{such that} \\
\enskipp \red{(} H 2 \red{)} $\,$(m\blue{=}(p\blue{+} x 0 )) \\
\enskipp \red{consider} $\,$H 1 \\
\enskipp \red{rewrite} m \red{with} (p\blue{+} x 0 ) by $\,$H 2 \\
\enskipp \red{we proved} (n\blue{=}((p\blue{+} x 0 )\blue{+}x)) \\
\enskipp \red{rewrite} ((p\blue{+} x 0 )\blue{+}x) \red{with} (p\blue{+}( x 0 \blue{+}x)) \red{by (}\blue{plus\_assoc\_l}{\dots}\red{)} \\
\enskipp \red{we proved} (n\blue{=}(p\blue{+}( x 0 \blue{+}x))) \\
\enskipp \red{by (}\blue{ex\_intro} . . . \red{previous)} \\
\enskipp \red{we proved} \blue{$\exists$}z:\blue{nat}.(n\blue{=}(p\blue{+}z)) \\
\enskipp \red{that is equivalent to} (n\blue{$\ge$}p) \\
\strut\red{we proved} \blue{$\forall$}n: \blue{nat} .\blue{$\forall$}m: \blue{nat} .\blue{$\forall$}p: \blue{nat} .\blue{$\forall$}H: (n\blue{$\ge$}m) .\blue{$\forall$} H 0 : (m\blue{$\ge$}p) .(n\blue{$\ge$}p)
\end{quote}
\vss}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch}
\green{proof: 5 lines of Mizar}
\begin{quote}
\textbf{definition let} n,m\textbf{;} \\
\quadskip \textbf{pred} n {\small $>$=} m \textbf{means} ex x st n = m + x\textbf{;} \\
\textbf{end;}
\end{quote}

\begin{quote}
\textbf{theorem} n {\small $>$=} m \& m {\small $>$=} p implies n {\small $>$=} p \\
\textbf{proof} \\
\quadskip \textbf{assume} n {\small $>$=} m \& m {\small $>$=} p\textbf{;} \\
\quadskip \textbf{consider} x \textbf{such that} n = m + x\textbf{;} \\
\quadskip \textbf{consider} x{\small 0} \textbf{such that} m = p + x{\small 0}\textbf{;} \\
%\quadskip n = m + x .= (p + x0) + x .= p + (x0 + x)\textbf{;} \\
\quadskip n = p + (x + x{\small 0})\textbf{;} \\
\quadskip \textbf{thus} n {\small $>$=} p\textbf{;} \\
\textbf{end;}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{differences between formal proof sketches and MoWGLI presentations?}
\begin{itemize}
\item[$+$]
formal proof sketches: \red{much smaller}
\item[$+$]
\advirecord{y1}{formal proof sketches: closer to informal textbook proofs}
\item[$+$]
\advirecord{y2}{formal proof sketches: written in \red{input language}}
\item[$-$]
\advirecord{y3}{formal proof sketches: can't be generated automatically} \\
\advirecord{y4}{(will need some human tagging)}
\end{itemize}
%\medskip
%
%\setbox0=\hbox{\textbf{much smaller than}}
%\textbf{presentation should be \advirecord{z1}{\rlap{\hbox to \wd0{at most as long as}}}\advirecord{z2}{\copy0} the formalization}
%\adviplay{z1}
%\adviwait
%\adviplay[white]{z1}\adviplay{z2}
%%\adviwait
%%
%%elements that are hidden in formal proof sketches:
%%\begin{itemize}
%%\item[$\bullet$]
%%labels and references to labels
%%\item[$\bullet$]
%%changes to the goal statement
%%\item[$\bullet$]
%%`in between' steps in the proof
%%\end{itemize}
\adviwait
\adviplay{y1}
\adviwait
\adviplay{y2}
\adviwait
\adviplay{y3}
%\adviwait
\adviplay{y4}
\adviwait
\medskip

\green{improving MoWGLI presentations through studying formal proof sketches}

\vspace{-2em}
\vfill
\end{slide}

\end{document}