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