\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xy}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.6}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\definecolor{slideorange}{rgb}{1,.5,0}
\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}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.8pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut two automation challenges}

\red{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

Dagstuhl seminar: \green{interaction versus automation} \\
{\small 2009\hspace{3pt}10\hspace{3pt}06, 17\hspace{1.5pt}:\hspace{1.5pt}00}

\end{slide}

\def\dummypic#1{\gray{\framebox(89.4,126.0){\black{#1}}}}
\def\pic#1{\includegraphics[width=89.4pt,height=126.0pt]{/home/freek/talks/automation/pics/#1.eps}}

\begin{slide}
\sectiontitle{automation}
\slidetitle{program verification versus mathematics}
\vspace{-.5em}
\begin{flushleft}
\hspace{3em}\pic{cs}\hspace{3em}\pic{math}
\end{flushleft}

\vfill
\end{slide}

\begin{slide}
\slidetitle{assistant versus word processor}
\vbox to 0pt{
\vspace{-.5em}
\begin{flushleft}
\hspace{3em}\pic{robot3}\hspace{3em}\pic{typewriter}\adviwait\rlap{\hspace{1em}\lower7em\hbox{\pic{iceberg}}}
\end{flushleft}
\vss
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{formal proof sketches}
\slidetitle{textbook proof from Hardy \& Wright}
\vspace{-1.2\medskipamount}

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}
\begin{center}
\setlength{\fboxsep}{.5em}
$\hspace{-2em}$\color{slidegray}\framebox{\color{black}\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}\color{slidegray}}\color{black}$\hspace{-2em}$
\end{center}
\end{quote}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch of the textbook proof}
\vspace{-1.2\medskipamount}

\vbox to 0pt{
\vspace{-1\bigskipamount}
\begin{quote}\small
\white{\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\rlap{;}}
\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 declarative formalization}
\vspace{-1.6\medskipamount}

\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{;}}\\
\blue{:: \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[slidegreen]{c6b}
\adviplay[slidegreen]{c7b}
\adviplay[slidegreen]{c10b}
\adviplay[slidegreen]{c11b}
\adviplay[slidegreen]{c11d}
\adviplay[slidegreen]{c12a}
\adviplay[slidegreen]{c13a}
\adviplay[slidegreen]{c13c}
\adviplay[slidegreen]{c34}
\adviplay[slidegreen]{c35a}
\adviplay[slidegreen]{c36}
\adviplay[slidegreen]{c40a}
\adviplay[slidegreen]{c41a}
\adviplay[slidegreen]{c41c}
\adviplay[slidegreen]{c46b}
\adviplay[slidegreen]{c46d}
\adviplay[slidegreen]{c51b}
\adviplay[slidegreen]{c51d}
\adviplay[slidegreen]{c53b}
\adviplay[slidegreen]{c53d}
\adviplay[slidegreen]{c54a}
\adviplay[slidegreen]{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{\textbf{first challenge: }automate elementary reasoning steps}

\blue{Larry Wos}\exclspace:
\vspace{-2em}
\begin{center}
\includegraphics[width=18em]{/home/freek/talks/automation/pics/ar.eps}
\end{center}
\vspace{-.8\bigskipamount}
\adviwait

\vbox to 0pt{
\begin{itemize}
\item[$\bullet$]
{{experience} with formal proof sketches\exclspace:} \\
\textsl{computers routinely proving \green{non-trivial} steps is far away}\toolong
\vspace{-\smallskipamount}
\adviwait

\item[$\bullet$]
focus should be on making \green{manual} math formalization \red{efficient}

\end{itemize}
\vss
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{luxury mathmode}
\slidetitle{procedural proof using tactics}
\hbox to 0pt{\vbox to 0pt{
\vspace{-1.25em}
\hfill{\includegraphics[width=6.5em]{/home/freek/talks/miz3/pics/proof.eps}\hspace{-2pt}}\strut
\vss}\hss}%
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
# \red{g `!n. nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2`;;}
val it : goalstack = 1 subgoal (1 total)\medskip
\green{`!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2`}\medskip
# \red{e INDUCT_TAC;;}
val it : goalstack = 2 subgoals (2 total)\medskip
  0 [`nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2`]\medskip
`nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2`\medskip
\green{`nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2`}\medskip
# \red{e (ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;}
val it : goalstack = 1 subgoal (2 total)\medskip
\green{`(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2`}\medskip
#
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{batch checked declarative proof}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
\red{!n. nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2}
proof
  {nsum(1..0) (\\i. i) = 0} \gray{by NSUM_CLAUSES_NUMSEG;}
    {\gray{...} = (0*(0 + 1))} DIV 2 \gray{[1];}
  now let n be num\gray{;}
    assume {nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2} \gray{[2];}
    {1 <= SUC n}\gray{;}
    {nsum(1..SUC n) (\\i. i) = (n*(n + 1)) DIV 2 + SUC n}
      \gray{by NSUM_CLAUSES_NUMSEG,2;}
    thus {\gray{...} = ((SUC n)*(SUC n + 1)) DIV 2}\gray{;}
  {end\gray{;}}
qed \gray{by {INDUCT_TAC},1;}
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{integrating the two worlds}

\textbf{Mizar Light} \\
= `\green{luxury mathmode}' (Henk) \\
= proof language/interface on top of HOL Light
\adviwait

\vspace{4em}
\begin{center}
\large
\blue{\textbf{demo}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{computer algebra with assumptions}
\slidetitle{two flavors of computer algebra}
\vspace{-1.5em}
$$
\hspace{2.5em}\xymatrix@R=0em@C=.5em{
 && *+<2.5em>{\hbox to 0em{\hss mathematical computation by computer\hss}}\ar[ddl]\ar[ddr] \\
\\
& *+<2.5em>{\hbox to 0em{\hss numerical computation\hss}} && *+<2.5em>{\hbox to 0em{\hss symbolic computation\adviwait\hss}}\ar[ddl]\ar[ddr] \\
\\
&& *+<2.5em>{\hbox to 0em{\hss computer algebra\hss}} && *+<2.5em>{\hbox to 0em{\hss\advirecord{a1}{computer calculus}\adviplay{a1}\hss}} \\\adviwait
\\
&& {\displaystyle{\red{1\over X}}} \in {\mathbb C}\;(X) && \lambda X\hspace{0pt}.\hspace{1.5pt}{\displaystyle{\red{1\over X}}} \in {\mathbb C\,\strut}^{{{\mathbb C}}_{\;\neq 0}} \\\adviwait
&& {\displaystyle{\red{X \over X}}} = 1\,\mbox{ \small as algebraic objects} && {\displaystyle{\red{X \over X}}} \neq 1\,\mbox{ {\small when} } X = 0
}\hspace{-2.5em}\adviwait\adviplay[slidegreen]{a1}
$$

\vspace{-19pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the Content MathML signature}
%
\def\x{\enskip\penalty100}%
\def\y{\mbox{\scriptsize\strut}\cdot}%
%
147 XML elements, like:

\gray{\fbox{\black{\parbox{29.8em}{%
\leftskip=.3em
\rightskip=0pt plus 1fil
$\displaystyle\strut
                                % cn
                                % ci
                                % csymbol
                                % apply
                                % reln
                                % fn
                                % interval
{^{-1}}\x                       % inverse
                                % sep
                                % condition
                                % declare
{\lambda}\x                     % lambda
{\circ}\x                       % compose
                                % ident
                                % domain
                                % codomain
                                % image
                                % domainofapplication
                                % piecewise
                                % piece
                                % otherwise
                                % quotient
{!}\x                           % factorial
{\div}\x                        % divide
{\max}\x                        % max
{\min}\x                        % min
{-}\x                           % minus
{+}\x                           % plus
                                % power
                                % rem
{\cdot}\x                       % times
{\sqrt{\phantom{\y}}}\x         % root
{\gcd}\x                        % gcd
{\land}\x                       % and
{\lor}\x                        % or
                                % xor
{\neg}\x                        % not
{\Rightarrow}\x                 % implies
{\forall}\x                     % forall
{\exists}\x                     % exists
{\left|\,\y\,\right|}\x         % abs
{\overline{\;\y\,}}\x           % conjugate
{\arg}\x                        % arg
{\Re}\x                         % real
{\Im}\x                         % imaginary
                                % lcm
{\lfloor\y\rfloor}\x            % floor
{\lceil\y\rceil}\x              % ceiling
{=}\x                           % eq
{\neq}\x                        % neq
{>}\x                           % gt
{<}\x                           % lt
{\geq}\x                        % geq
{\leq}\x                        % leq
{\Leftrightarrow}\x             % equivalent
{\approx}\x                     % approx
{\,|\,}\x                       % factorof
{\int}\x                        % int
{{d}\over{d}x}\x                % diff
{\partial\over\partial x}\x     % partialdiff
                                % lowlimit
                                % uplimit
                                % bvar
                                % degree
{\nabla}\x                      % divergence
                                % gradient
                                % curl
                                % laplacian
                                % set                  
                                % list                 
{\cup}\x                        % union
{\cap}\x                        % intersect
{\in}\x                         % in
                                % notin
{\subseteq}\x                   % subset
{\subset}\x                     % prsubset
                                % notsubset
                                % notprsubset
{\backslash}\x                  % setdiff
{\#}\x                          % card
{\times}\x                      % cartesianproduct
{\textstyle\sum}\x              % sum
{\textstyle\prod}\x             % product
{\lim}\x                        % limit
                                % tendsto
                                % exp
\strut%\penalty-100\strut
{\ln}\x                         % ln
{\log}\x                        % log
                                % logbase
{\sin}\x                        % sin
{\cos}\x                        % cos
{\tan}\x                        % tan
{\sec}\x                        % sec
{\csc}\x                        % csc
{\cot}\x                        % cot
{\sinh}\x                       % sinh
{\cosh}\x                       % cosh
{\tanh}\x                       % tanh
                                % sech
                                % csch
{\coth}\x                       % coth
{\arcsin}\x                     % arcsin
{\arccos}\x                     % arccos
{\arctan}\x                     % arctan
                                % arccot
                                % arccsc
                                % arcsec
                                % arccosh
                                % arccoth
                                % arccsch
                                % arcsech
                                % arcsinh
                                % arctanh
\strut%\penalty-100\strut
{\mu}\x                         % mean
{\sigma}\x                      % sdev
                                % variance
                                % median
                                % mode
                                % moment
                                % momentabout
                                % vector
                                % matrix
                                % matrixrow
{\det}\x                        % determinant
{^{\rm T}}\x                    % transpose
                                % selector
                                % vectorproduct
                                % scalarproduct
{\otimes}\x                     % outerproduct
                                % annotation           
                                % semantics            
                                % annotation-xml       
{\mathbb Z}\x                   % integers
{\mathbb R}\x                   % reals
{\mathbb Q}\x                   % rationals
{\mathbb N}\x                   % naturalnumbers
{\mathbb C}\x                   % complexes
                                % primes
{\,e}\x                           % exponentiale
{i}\x                           % imaginaryi
                                % notanumber
{\top}\x                        % true
{\bot}\x                        % false
{\emptyset}\x                   % emptyset
{\pi}\x                         % pi
{\gamma}\x                      % eulergamma
{\infty}                        % infinity
\strut$
}}}}$\hspace{-2em}$
\bigskip
\adviwait

\vbox to 0pt{
\small
\setlength{\tabcolsep}{1em}
\gray{%
\begin{tabular}{c|lll}
& \black{MathML} & \black{\LaTeX} & \black{HOL} \\
\hline
\black{$p \Rightarrow q$} & \black{\texttt{implies}} & \black{\texttt{\char`\\Rightarrow}}$\enskip$ & \black{\texttt{==>}} \\
\noalign{\vspace{-\smallskipamount}}
%\black{$x \in A$} & \black{\texttt{in}} & \black{\texttt{\char`\\in}} & \black{\texttt{IN}} \\
%\noalign{\vspace{-\smallskipamount}}
\black{$A \times B$} & \black{\texttt{cartesianproduct}} & \black{\texttt{\char`\\times}} & \black{\texttt{prod}$\,,\;$\texttt{CROSS}} \\
\noalign{\vspace{-\smallskipamount}}
%\black{${f^{-1}}$} & \black{\texttt{inverse}} & & \black{\texttt{inverse}} \\
%\noalign{\vspace{-\smallskipamount}}
\black{$0$} & \black{\texttt{cn}} & & \black{\texttt{NUMERAL}} \\
\noalign{\vspace{-\smallskipamount}}
%\black{$\sqrt{x}$} & \black{\texttt{root}} & \black{\texttt{\char`\\sqrt}} & \black{\texttt{sqrt}$\,,\;$\texttt{csqrt}} \\
%\noalign{\vspace{-\smallskipamount}}
\black{$\sum_{i = 1}^n a_i$} & \black{\texttt{sum}} & \black{\texttt{\char`\\sum}} & \black{\texttt{nsum}$\,,\;$\texttt{sum}} \\
\noalign{\vspace{-\smallskipamount}}
%\black{$x \approx y$} & \black{\texttt{approx}} & \black{\texttt{\char`\\approx}} & \\
%\noalign{\vspace{-\smallskipamount}}
\black{$\infty$} & \black{\texttt{infinity}} & \black{\texttt{\char`\\infty}} & \\
\end{tabular}\toolong
}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{sample problem}
\vspace{0pt}

\begin{center}
%\strut\toolong
$\displaystyle {x \ne 0 \;\,\land\,\; \big|\ln(x^2)\big| > 1 \,\;\land\,\, \int_0^x t\, dt \le 1 \;\,\Rightarrow\;\, -{1\over\sqrt{e}} < x < {1\over\sqrt{e}}}
%\approx 0.60653065\hspace{1pt}\rlap{\dots}$\toolong\strut
$
\end{center}
\bigskip
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\textsl{this is not about first order proof search}

first order proof search cannot easily calculate integrals \\
first order proof search cannot easily do numerical approximations
\smallskip
\adviwait

\item[$\bullet$]
\textsl{this is not about decision procedures}

decision procedures generally work over specific small signatures
\smallskip
\adviwait

\item[$\bullet$]
\textsl{this is not about systems like Maple and Mathematica}\toolong

current computer algebra systems generally do not use assumptions

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{second challenge: }take next step in mathematics automation}
\vspace{-1.44em}%\adviwait

\blue{progress\exclspace:} %in proof assistant technology\exclspace:}
\begin{itemize}
\item[$\bullet$]
automation of formalized \green{primary school} math = `arithmetic'

\item[$\bullet$]
\red{\advirecord{e1}{automation of formalized \advirecord{e2}{high school}\adviplay[slidegreen]{e2} math}}\adviplay{e1} = `calculus'

\item[$\bullet$]
automation of formalized \green{university} math

\end{itemize}
\bigskip
\adviwait
\adviplay[slidered]{e1}
\adviplay[slidered]{e2}
\adviwait

should run in \red{less than a second}
\bigskip
\adviwait

should run \green{without any arguments} \\\adviwait
should \red{implicitly} use\exclspace:
\begin{itemize}
\item[$\bullet$]
assumptions in the goal = local labels in the proof

\item[$\bullet$]
theorems from the formal library

\end{itemize}

\vspace{-12pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the plan}
\slidetitle{creating a collection of mathematical problems}
\vbox to 0pt{
\vspace{-.7em}
\hfill\pic{pftb}\hspace{-3em}\strut
\vss}
\vspace{-2.85em}
\begin{itemize}
\item[$\bullet$]
take proofs from \textbf{Proofs from The Book}
\begin{picture}(50,5)\put(0,2.4){\gray{\vector(1,0){44.5}}}\end{picture}
\adviwait

\item[$\bullet$]
create \textbf{formal proof sketches} of those proofs
\adviwait

\item[$\bullet$]
calculate the \textbf{proof obligations} of the steps in \\ those formal proof sketches
\adviwait

\item[$\bullet$]
select proof obligations in the \textbf{Content MathML} \\ {signature}
\adviwait

\end{itemize}

\bigskip
\bigskip
\bigskip
\begin{center}
\large
\blue{\textbf{benchmark for math automation}}
\end{center}

\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof obligations for the Hardy \& Wright example}
\begin{eqnarray*}
\sqrt{2}\in {\mathbb Q} &\red{\vdash}& \exists\, a,b\in{\mathbb Z}\, (a^2 = 2 b^2 \,\land\; {\sf gcd}(a,b) = 1)\hspace{-.2em} \\
b\in{\mathbb Z} \,\land\, a^2 = 2 b^2 &\red{\vdash}& 2 \mathrel{|} a^2 \\
a\in{\mathbb Z} \,\land\, 2 \mathrel{|} a^2 &\red{\vdash}& 2 \mathrel{|} a \\
2 \mathrel{|} a &\red{\vdash}& \exists\,c\in{\mathbb Z}\, (a = 2 c) \\
a^2 = 2 b^2 \,\land\, a = 2 c &\red{\vdash}& 4 c^2 = 2 b^2 \\
4 c^2 = 2 b^2 &\red{\vdash}& 2 c^2 = b^2 \\
b\in{\mathbb Z} \,\land\, c\in{\mathbb Z} \,\land\, 2 c^2 = b^2 &\red{\vdash}& 2 \mathrel{|} b \\
\hspace{.2em}{\sf gcd}(a,b) = 1 \,\land\, 2 \mathrel{|} a \,\land\, 2 \mathrel{|} b &\red{\vdash}& \bot
\adviwait
\end{eqnarray*}

\green{{Content MathML} signature} \\
\adviwait
{only relevant subset of the assumptions shown here}
\adviwait

\red{each should be {proved automatically} in less than a second\exclspace!}

\vspace{-10pt}
\vfill
\end{slide}

\end{document}

\begin{slide}
\slidetitle{some proof obligations for the summation example}
\begin{eqnarray*}
&\red{\vdash}& \sum_{i = 1}^0 i = 0 \\
\sum_{i = 1}^n i = {n (n + 1)\over 2} &\red{\vdash}& \sum_{i = 1}^{n + 1} i = {n (n + 1)\over 2} + n + 1 \\
&\red{\vdash}& {n (n + 1)\over 2} + n + 1 = {(n + 1) ((n + 1) + 1)\over 2} \\
%\noalign{\bigskip\adviwait}
%\gray{\sum_{i = 1}^0 i = 0 \,\land {} \hspace{10em}} \\
%\noalign{\vspace{-2\smallskipamount}}
%\gray{\forall n\in{\mathbb N}\,.\, \sum_{i = 1}^n i = {n (n + 1)\over 2} \,\Rightarrow\quad} \\
%\noalign{\vspace{-2\smallskipamount}}
%\gray{\sum_{i = 1}^{n + 1} i = {(n + 1) ((n + 1) + 1)\over 2}} &\red{\vdash}& \gray{\sum_{i = 1}^n i = {n (n + 1)\over 2}}
\end{eqnarray*}

\vspace{-12pt}
\vfill
\end{slide}

\end{document}
