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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidelightgray}{rgb}{.8,.92,.8}
\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}{\strut #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}
\newcommand{\toolong}{$\hspace{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large proof assistants for mathematics}

Freek Wiedijk \\
Radboud University, Nijmegen \\
Free University, Amsterdam

OzsL Schoolweek \\
Hotel Dennenhoeve, Nunspeet \\
2004 12 02, 15:30
\end{slide}

\begin{slide}
\sectiontitle{intro}
\slidetitle{the best of two worlds}
formalizing proofs is like
\begin{itemize}
\item[$\bullet$]
  \textbf{programming} \\ but no bugs, and not trivial
\item[$\bullet$]
  \textbf{doing mathematics} \\ but transparent, and the computer helps
\end{itemize}
\adviwait

\green{(currently closer to programming than to doing mathematics)}
\adviwait

\begin{center}
\bigskip
\red{a wonderful computer game\exclspace!}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{systems}
\slidetitle{mathematics in the computer}
\begin{itemize}
\item[$\bullet$] \textbf{numerical}
\begin{center}
\advirecord{d1}{calculations}\advirecord{d2}{\llap{numbers}}\adviplay{d1}: computer $\to$ human$\qquad$
\end{center}
\adviwait

\item[$\bullet$] \textbf{computer algebra}
\begin{center}
\advirecord{d3}{calculations}\advirecord{d4}{\llap{formulas}}\adviplay{d3}: computer $\to$ human$\qquad$
\end{center}
\adviwait
\adviplay[white]{d1}
\adviplay{d2}
\adviplay[white]{d3}
\adviplay{d4}
\adviwait

\item[$\bullet$] \textbf{automated theorem provers}
\begin{center}
proofs: computer $\to$ human
\end{center}
\adviwait

\item[$\bullet$] \textbf{\advirecord{c}{proof assistants}\adviplay{c}}
\begin{center}
proofs: human $\to$ computer
\smallskip
\adviwait
\adviplay[slidered]{c}
\end{center}
\begin{flushright}
\green{(computer just checks whether the proof is correct)}
\end{flushright}

\end{itemize}

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

\begin{slide}
\slidetitle{the two kinds of computer proof}

\begin{itemize}
\item[$\bullet$]
\textbf{correctness of computer software and hardware}

\green{(serious branch of computer science: `formal methods')}
\smallskip

statements\exclspace: big \\
proofs\exclspace: shallow \\
computer does the main part of the proof
\bigskip
\adviwait

\item[$\bullet$]
\textbf{correctness of \advirecord{a}{mathematical theorems}\adviplay{a}}

\green{(slow and thorough style of doing mathematics, still in its infancy)}
\smallskip

statements\exclspace: small \\
proofs\exclspace: deep \\
human does the main part of the proof

\end{itemize}
\adviwait
\adviplay[slidered]{a}

\vfill
\end{slide}

\begin{slide}
\slidetitle{prehistory}
\begin{center}
\begin{tabular}{rl}
1968 & \textbf{Automath} \\
& Netherlands, de Bruijn \\
\noalign{\medskip}
1971 & \textbf{nqthm} \\
& US, Boyer \& Moore \\
\noalign{\medskip}
1972 & \textbf{LCF} \\
& UK, Milner \\
\noalign{\medskip}
1973 & \textbf{Mizar} \\
& Poland, Trybulec
\end{tabular}
$\qquad$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the seven provers of the world}
\vspace{-2\bigskipamount}

\begingroup
\small
$$\hspace{-8.5em}\xymatrix{
\txt{\advirecord{a1}{Mizar}\adviplay{a1}}\ar@(dr,ul)[rrrd]\ar@{.}[rrrr] &&&& \txt{\rlap{\green{\textsl{most mathematical}}}} \\
\txt{\gray{LCF}}\ar[rr]\ar[rrd]\ar@/_1.8pc/[rrrdd] && \txt{\advirecord{a2}{HOL}\adviplay{a2}}\ar[r] & \txt{Isabelle}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most pure}}}} \\
\txt{\gray{Automath}}\ar[rr] && \txt{$\,$\advirecord{a3}{\rlap{Coq}\phantom{NuPRL}}\adviplay{a3} \\\noalign{\smallskip} NuPRL$\!$}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most logical}}}} \\
&&& \txt{PVS}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most popular}}}} \\
\txt{\gray{nqthm}}\ar[rr]\ar@/^.5pc/[rrru] && \txt{ACL2}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most computational}}}} \\
}
\adviwait
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}
\adviplay[slideblue]{a3}
$$
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{foundations}
\begin{itemize}
\item[$\bullet$]
\textbf{primitive recursive arithmetic}

ACL2

\item[$\bullet$]
\textbf{type theory}

\green{typed lambda calculus + inductive types, constructive}

\blue{Coq}, NuPRL

\item[$\bullet$]
\textbf{higher order logic}

\green{typed lambda calculus + choice operator, classical}

\red{HOL}, Isabelle, PVS

\item[$\bullet$]
\textbf{set theory}

\red{Mizar}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural versus declarative}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\green{
\begin{picture}(5,5)
\advirecord{e0}{
\put(0,5){\line(1,0){5}}
\put(.5,4.5){\makebox(0,0){\black{\scriptsize $0$}}}
\put(0,4){\line(1,0){3}}
\put(1,3){\line(1,0){2}}
\put(2,2){\line(1,0){1}}
\put(4,2){\line(1,0){1}}
\put(3,1){\line(1,0){2}}
\put(4.5,.5){\makebox(0,0){\black{\scriptsize $\infty$}}}
\put(0,0){\line(1,0){5}}
\put(0,0){\line(0,1){5}}
\put(1,1){\line(0,1){2}}
\put(2,0){\line(0,1){1}}
\put(3,1){\line(0,1){2}}
\put(4,2){\line(0,1){2}}
\put(5,0){\line(0,1){5}}
}
\adviplay[slidegreen]{e0}
\put(0.2,4.5){\makebox(0,0){\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,4.5){\makebox(0,0){\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,4.5){\makebox(0,0){\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,4.5){\makebox(0,0){\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,3.5){\makebox(0,0){\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,3.5){\makebox(0,0){\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,3.5){\makebox(0,0){\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,3.5){\makebox(0,0){\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,2.5){\makebox(0,0){\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,1.5){\makebox(0,0){\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,0.5){\makebox(0,0){\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,0.5){\makebox(0,0){\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,1.5){\makebox(0,0){\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,1.5){\makebox(0,0){\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,0.5){\makebox(0,0){\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,0.5){\makebox(0,0){\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}
\put(4.2,0.5){\makebox(0,0){\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}
\end{picture}
}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%

\begin{itemize}
\item[$\bullet$]
\textbf{procedural}

\begingroup
\small
\green{%
\adviwait
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
E
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
E
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
S
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
E
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
N
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
E
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
S
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
S
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
S
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
W
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
W
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
W
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
S
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
E
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
E
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
E
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidegreen]{e0}
}
\endgroup

\red{HOL}, PVS, \blue{Coq}, NuPRL

\adviwait
\item[$\bullet$]
\textbf{declarative}

\begingroup
\scriptsize
\green{
\adviwait
(0,0)
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
(1,0)
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
(2,0)
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
(3,0)
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
(3,1)
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
(2,1)
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
(1,1)
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
(0,1)
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
(0,2)
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
(0,3)
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
(0,4)
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
(1,4)
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
(1,3)
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
(2,3)
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
(2,4)
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
(3,4)
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
(4,4)
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%
}\toolong
\endgroup

\red{Mizar}, Isabelle

\end{itemize}

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

\begin{slide}
\slidetitle{the best prover of the world?}
\begin{center}
\includegraphics[190,590][430,730]{/home/freek/talks/school/diag2.ps}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the example}
\slidetitle{a small proof}

\textbf{Theorem. }%
\textsl{There are irrational numbers \red{$x$} and \red{$y$}
such that \green{$x^y$} is rational.\adviwait}

\textbf{Proof. }%
We have the following calculation
$${\big(\sqrt{2}^{\sqrt{2}}\rlap{$\big)$}{\scriptscriptstyle\strut}}^{\sqrt{2}} =
\sqrt{2}^{\sqrt{2}\cdot\sqrt{2}} =
\sqrt{2}^{\,2} =
\green{2}$$
which is rational.
\adviwait
Furthermore Pythagoras showed that \red{$\sqrt{2}$} is irrational.
\adviwait
Now there are two cases:
\begin{itemize}
\item[$\bullet$]
Either \green{$\sqrt{2}^{\sqrt{2}}$} is rational.
\advirecord{f1}{Then take $\red{x = y = \sqrt{2}}$.}

\item[$\bullet$]
Or $\red{\sqrt{2}^{\sqrt{2}}}$ is irrational.
\advirecord{f2}{In that case take \red{$x = \sqrt{2}^{\sqrt{2}}$} and \red{$y = \sqrt{2}$}.
And by the above calculation then \green{$x^y = 2$}, which is rational.
\hfill$\Box$}

\end{itemize}
\adviwait
\adviplay{f1}
\adviwait
\adviplay{f2}
%\adviwait
%(Note that the proof doesn't say which of the two cases holds!)

%\vspace{-11pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{HOL proof}
\slidetitle{the Pentium bug}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/dagen/pics/pentium.eps}}
\vss
}
Pentium: Intel processor
\medskip
\adviwait

mid 1994: processor makes errors \\
\red{FDIV bug}, not enough precision
\medskip

$\sf {5505001\over 294911} = 18.66665197$\dots\hspace{.8em}\green{(mathematics)}

$\sf {5505001\over 294911} = 18.66600093$\dots\hspace{.8em}\green{(Pentium)}
\bigskip
\adviwait

Intel: processor that has bug will be replaced for free \\
\red{estimated damage: 475 million dollars}

\vfill
\end{slide}

\begin{slide}
\slidetitle{John Harrison and HOL Light}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/school/johnh.eps}}
\vss
}
John Harrison\exclspace: \\
reimplementation of the HOL system
\medskip

\qquad LCF $\to$ HOL $\to$ \red{HOL Light}
\bigskip
\adviwait

PhD in Cambridge, UK \\
\textbf{formalization of mathematics}

\green{e.g. fundamental theorems of calculus \& algebra}

\red{Flyspeck project}
%(all by himself,
%all the way down to the HOL axioms)
\medskip
\adviwait

currently works at Intel \\
\textbf{verification of the real thing}

\green{floating point algorithms in the actual Intel chips}

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

\begin{slide}
\slidetitle{the proof: \textbf{in the file}}
{one bead on the necklace}
\medskip

\begingroup
\small
\def\\{\char`\\}
\begin{alltt}
let \green{EXAMPLE} = {prove}
 {(}\red{`?x y. ~rational x /\\ ~rational y /\\ rational(x^y)`}{,}
  \blue{\blue{ASM_CASES_TAC `rational(sqrt(&2)^sqrt(&2))`} {THENL}
   {[}\blue{EXISTS_TAC `sqrt(&2)`}{;} \blue{EXISTS_TAC `sqrt(&2)^sqrt(&2)`}{]} {THEN}
  \blue{EXISTS_TAC `sqrt(&2)`} {THEN}
  \blue{ASM_SIMP_TAC[SQRT_POW_2; GSYM REAL_POW_2; REAL_OF_NUM_LE; ARITH;\toolong
               REAL_OF_NUM_LT; REAL_POWER_POW; SQRT_POS_LT;
               REAL_POWER_POWER; SQRT_2_IRRATIONAL; RATIONAL_NUM]}}{)};;\toolong
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural proof: shooting at subgoals}

\begin{itemize}
\item[$\bullet$]
\textbf{goal} \\
\green{`proof obligation'}

that what is left to be proved
\medskip

\item[$\bullet$]
\textbf{tactic} \\
\green{command that proves part of a goal}

reduces the goal to zero or more new `subgoals'

\end{itemize}

\begin{center}
\bigskip
\red{proving is a computer game\exclspace!}
\medskip
\end{center}

\strut\phantom{theorems}\llap{goals} $\;$are like$\;$ monsters \\
\phantom{theorems}\llap{tactics} $\;$are like$\;$ guns \\
theorems $\;$are like$\;$ game levels

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

\def\Implies{\,\Rightarrow\,}
\def\Iff{\,\Leftrightarrow\,}
\def\_{\char`\_}
\def\^{\char`\^}

\begin{slide}
\slidetitle{lemmas and tactics}
the HOL Light library consists of
\begin{itemize}
\item[$\bullet$]
\textbf{lemmas} \\
\green{proven statements}
\medskip

\red{declarative knowledge}
\medskip

basic library: 1501 lemmas

from
\blue{$\,\vdash\top \!\Iff \lambda x^{\mathbb B}.\, x = \lambda x^{\mathbb B}.\, x\,$}
to
\blue{$\,\vdash\forall x\,\forall y.\, x = y \Iff x_1 = y_1 \land x_2 = y_2\,$}\toolong
\medskip

\item[$\bullet$]
\textbf{tactics} \\
\green{small programs that know how to prove things}
\medskip

\red{procedural knowledge}
\medskip

basic library: 128 tactics

\end{itemize}

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

\begin{slide}
\slidetitle{lemmas used in the proof}
\begin{center}
\begin{tabular}{lcc}
{\texttt{SQRT\_2\_IRRATIONAL}} &$\qquad$& {$\sqrt{2} \not\in {\mathbb Q}$} \\
\texttt{RATIONAL\_NUM} && $\bar{n} \in {\mathbb Q}$ \\
\noalign{\medskip}
\texttt{REAL\_POWER\_POWER} && $(x^y)^z = x^{y z}$ \\
\texttt{SQRT\_POW\_2} && $\bar{0} \le x \Implies (\sqrt{x})^2 = x$ \\
\texttt{REAL\_POW\_2} && $x^2 = x\cdot x$ \\
\texttt{REAL\_POWER\_POW} && $\bar{0} < x \Implies x^{\bar{n}} = x^n$ \\
\texttt{SQRT\_POS\_LT} && $\bar{0} < x \Implies \bar{0} < \sqrt{x}$ \\
\texttt{REAL\_OF\_NUM\_LE} && $\bar{m} \le \bar{n} \Iff m \le n$ \\
\texttt{REAL\_OF\_NUM\_LT} && $\bar{m} < \bar{n} \Iff m < n$ \\
\noalign{\medskip}
\texttt{ARITH} && \green{very long statement}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the equality}
\vbox to 0pt{
\vspace{-2\bigskipamount}
\begingroup
\scriptsize
\let\small=\scriptsize
$$\hspace{-3em}\xymatrix@C=.5em@R=4em{
& && && && \ar[d]|-{\texttt{\strut\small ARITH}} && \\
& && && \strut\ar[d]|-{\texttt{\strut\small ARITH}} && \strut\green{0 < 2}\ar[d]|-{\texttt{\strut\small REAL\_OF\_NUM\_LT}} && \strut\ar[d]|-{\texttt{\strut\small ARITH}} \\
& && && \strut\green{0 \le 2}\ar[d]|-{\texttt{\strut\small REAL\_OF\_NUM\_LE}} && \strut\green{\bar{0} < \bar{2}}\ar[d]|-{\texttt{\strut\small SQRT\_POS\_LT}} && \strut\green{0 \le 2}\ar[d]|-{\texttt{\strut\small REAL\_OF\_NUM\_LE}} \\
& \ar[d]|-{\texttt{\strut\small REAL\_POWER\_POWER}} && \ar[d]|-{\texttt{\strut\small REAL\_POW\_2}} && \strut\green{\bar{0} \le \bar{2}}\ar[d]|-{\texttt{\strut\small SQRT\_POW\_2}} && \strut\green{\bar{0} < \sqrt{\bar{2}}}\ar[d]|-{\texttt{\strut\small REAL\_POWER\_POW}} && \strut\green{\bar{0} \le \bar{2}}\ar[d]|-{\texttt{\strut\small SQRT\_POW\_2}} \\
\red{(\sqrt{\bar{2}}^{\sqrt{\bar{2}}})^{\sqrt{\bar{2}}\strut}} & \mathrel{\red{=}}^{\strut} & \red{\sqrt{\bar{2}}^{\sqrt{\bar{2}} \cdot \sqrt{\bar{2}}\strut}} & \mathrel{\green{=}}^{\strut} & \green{\sqrt{\bar{2}}^{\sqrt{\bar{2}}^2\strut}} & \mathrel{\red{=}}^{\strut} & \red{\sqrt{\bar{2}}^{\bar{2}\strut}} & \mathrel{\green{=}}^{\strut} & \green{\sqrt{\bar{2}}^{2\strut}} & \mathrel{\red{=}}^{\strut} & \red{\bar{2}^{\strut}}
}\hspace{-3em}$$
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{tactics used in the proof}
\begin{itemize}
\item[$\bullet$]
\red{\texttt{ASM\_CASES\_TAC}}

\green{do a case split according to whether a given statement is true or false}\toolong

\item[$\bullet$]
\red{\texttt{EXISTS\_TAC}}

\green{prove an existential statement by providing a witness}

\item[$\bullet$]
\texttt{REWRITE\_TAC} \\
\texttt{SIMP\_TAC} \\
\texttt{ASM\_REWRITE\_TAC} \\
\red{\texttt{ASM\_SIMP\_TAC}}

\green{rewrite the goal according to a set of lemmas}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof: \textbf{interactively}}
\bigskip

\begin{center}
\large
\gray{DEMO}
\end{center}
\vspace{4\bigskipamount}

\strut\quad\textbf{commands}
\begin{itemize}
\item[]
\red{\texttt{g}}\qquad
set the \red{g}oal

\item[]
\red{\texttt{e}}\qquad
\red{e}xecute a tactic

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{HOL architecture}
\slidetitle{types and terms}
\begin{itemize}
\item[$\bullet$]
\textbf{types}
$$\rlap{$\green{\sigma \quad::=\quad \alpha \quad|\quad (\sigma_1,\dots,\sigma_n)\,\mbox{\red{op}}}$}\phantom{t \quad::=\quad x \quad|\quad \mbox{\red{c}} \quad|\quad t\;t' \quad|\quad \lambda x.\, t}\medskip$$
\strut\hspace{6em}\begin{tabular}{rr}
$\sigma_1\to\sigma_2$ & $(\sigma_1,\sigma_2)\,\mbox{\red{fun}}$ \\
\phantom{choice operator}\llap{{truth values}} & $()\,\mbox{\red{bool}}$ \\
{`individuals'} & $()\,\mbox{\red{ind}}$
\end{tabular}

\item[$\bullet$]
\textbf{terms}
$$\green{t \quad::=\quad x \quad|\quad \mbox{\red{c}} \quad|\quad t\;t' \quad|\quad \lambda x.\, t}\medskip$$
\strut\hspace{6em}\begin{tabular}{rl}
{equality} & \texttt{\red{=}} \\
{choice operator} & \texttt{\red{@}}
\end{tabular}

\end{itemize}

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

\begin{slide}
\slidetitle{the ten deduction rules of the HOL logic}
\begin{itemize}
\item[$\bullet$]
\texttt{REFL}

\item[$\bullet$]
\texttt{TRANS}

\item[$\bullet$]
\texttt{MK\_COMB}

\item[$\bullet$]
\texttt{ABS}

\item[$\bullet$]
\texttt{BETA}

\item[$\bullet$]
\texttt{ASSUME}

\item[$\bullet$]
\texttt{EQ\_MP}

\item[$\bullet$]
\texttt{\advirecord{g}{DEDUCT\_ANTISYM\_RULE}\adviplay{g}}

\item[$\bullet$]
\texttt{INST}

\item[$\bullet$]
\texttt{INST\_TYPE}

\end{itemize}
\adviwait
\adviplay[slidered]{g}

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

\begin{slide}
\slidetitle{example of a HOL rule: \texttt{DEDUCT\_ANTISYM\_RULE}}
version from the manual \& the implementation

$$
{
\strut
\Gamma \vdash p
\qquad
\Delta \vdash q
\over
\strut
(\Gamma - \{q\}) \cup (\Delta - \{p\}) \,\vdash\, p = q
}
\rlap{\enskip
\texttt{\small\red{DEDUCT\_ANTISYM\_RULE}}
}
\hspace{6em}
$$
\bigskip
\adviwait

\green{didactic version}
\vspace{-\medskipamount}

$$
\green{
{
\strut
\Gamma \cup \{q\} \vdash p
\qquad
\Delta \cup \{p\} \vdash q
\over
\strut
\Gamma \cup \Delta \,\vdash\, p = q
}
\hspace{6em}
}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{definitions}
\begin{itemize}
\item[$\bullet$]
\textbf{term definition}

introduction of new term constant $\,$\red{c}$\,$ to the signature \\
\green{abbreviates an existing term}
\medskip

\item[$\bullet$]
\textbf{type definition}

introduction of new {type constant} $\,$\red{op}$\,$ to the signature \\
\green{cuts out part from an existing type}

\vbox to 0pt{
\begin{flushright}
\includegraphics[bbllx=100,bburx=450,bblly=250,bbury=350,scale=.7]{/home/freek/talks/school/newtype.eps}
\end{flushright}
\vss
}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{functional programming will save the world}
\textbf{spin-off} technology

\begin{center}
proof verification \\
LCF

$\downarrow$

\textbf{functional programming} \\
\red{\textbf{ML}} \\
\green{meta-language}

(originally: the language for programming LCF tactics)
\bigskip
\end{center}

\red{different programming paradigm} \\
Lisp, ML, Haskell

\vfill
\end{slide}

\begin{slide}
\slidetitle{the HOL kernel}
HOL Light is an \green{ML program}
\medskip

\begin{center}
\begin{tabular}{lrr}
source of the whole system$\quad$ & 62,642 lines of code & 930 pages \\
\quad \green{75 files} \\
\noalign{\medskip}
\adviwait
\red{source of the kernel} & \red{643 lines of code} & \red{10 pages} \\
\quad \green{\texttt{type.ml}} & 135 lines of code & 2 pages \\
\quad \green{\texttt{term.ml}} & 279 lines of code & 4 pages \\
\quad \green{\texttt{thm.ml}} & 229 lines of code & 4 pages%
\adviwait
\end{tabular}
\end{center}
\bigskip

\blue{de Bruijn criterion}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the three basic HOL types}
{three datatypes in the implementation} \\
{(all three are \textbf{syntactic trees} represented in the computer memory)}
\bigskip

\begin{alltt}
type \blue{hol_type} = Tyvar of string
              | Tyapp of string * \blue{hol_type} list
\end{alltt}
\medskip

\begin{alltt}
type     \red{term} = Var of string * \blue{hol_type}
              | Const of string * \blue{hol_type}
              | Comb of \red{term} * \red{term}
              | Abs of \red{term} * \red{term}
\end{alltt}
\medskip

\begin{alltt}
type      \green{thm} = Sequent of (\red{term} list * \red{term})
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{implementation of \texttt{DEDUCT\_ANTISYM\_RULE}}

$$
{
\strut
\blue{\Gamma \vdash p}
\qquad
\blue{\Delta \vdash q}
\over
\strut
\green{(\Gamma - \{q\}) \cup (\Delta - \{p\}) \,\vdash\, p = q}
}
\rlap{\enskip
\texttt{\small\red{DEDUCT\_ANTISYM\_RULE}}
}
\hspace{6em}
$$
\bigskip
\adviwait

\begingroup
\small
\begin{alltt}
let \red{DEDUCT_ANTISYM_RULE} \blue{(Sequent(asl1,c1))} \blue{(Sequent(asl2,c2))} =
  let asl1' = filter (not o (aconv c2)) asl1
  and asl2' = filter (not o (aconv c1)) asl2 in
  \green{Sequent(term_union asl1' asl2',mk_eq(c1,c2))};;
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar proof}
\slidetitle{Andrzej Trybulec and Mizar}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=10em]{/home/freek/talks/school/andrzej.eps}}
\vss
}
Mizar: second star in the big dipper \\
\green{system from Bia{\l}ystok, Poland}
\medskip

motivated from \red{mathematics} \\
instead of from computer science
\medskip

\strut\phantom{+} first order predicate logic \\
+ axiom schemes \\
+ \red{ZFC set theory} \\
+ arbitrarily large inaccessible cardinals
\medskip

implemented in \red{Pascal} \\
source code not freely accessible to just anyone

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

\begin{slide}
\slidetitle{the proof: \textbf{in the file}}
\vbox to 0pt{
\vspace{-\bigskipamount}
\begingroup
\small
\begin{alltt}
theorem \green{Example:} \red{ex x, y being real number st
  x is irrational & y is irrational & x to_power y is rational}
proof
\blue{ set w = sqrt 2; w > 0 \gray{by AXIOMS:22,SQUARE_1:84};
 then \gray{A1:} (w to_power w) to_power w = w to_power (w * w) \gray{by POWER:38}\toolong
  .= w to_power (w^2) \gray{by SQUARE_1:def 3}
  .= w to_power 2 \gray{by SQUARE_1:def 4}
  .= w^2 \gray{by POWER:53}
  .= 2 \gray{by SQUARE_1:def 4};
 per cases;
 suppose \gray{A2:} w to_power w is rational;
  take w, w; thus thesis \gray{by A2,IRRAT_1:1,INT_2:44};
 end;
 suppose \gray{A3:} w to_power w is irrational;
  take w to_power w, w; thus thesis \gray{by A1,A3,IRRAT_1:1,INT_2:44};
 end;}
end;
\end{alltt}
\endgroup
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{lemmas used in the proof}
\begin{center}
\begin{tabular}{lcc}
\texttt{AXIOMS:22} &$\qquad$& $x \le y \,\land\, y \le z \Implies x \le z$ \\
\texttt{INT\_2:44} && $2\mbox{ is prime}$ \\
\texttt{IRRAT\_1:1} && $p\mbox{ is prime} \Implies \sqrt{p} \not\in {\mathbb Q}$ \\
\texttt{POWER:38} && $a > 0 \Implies {(a^b)}^c = a^{bc}$ \\
\texttt{SQUARE\_1:def 3} && $\red{x^2} = x \cdot x$ \\
\texttt{SQUARE\_1:def 4} && $0 \le a \Implies (x = \red{\sqrt{a}} \Iff 0 \le x \,\land\, x^2 = a)$ \\
\texttt{SQUARE\_1:84} && $1 < \sqrt{2}$ \\
\noalign{\medskip\adviwait}
\texttt{POWER:53} && \green{\texttt{a to\_power 2 = a\^2}}
\end{tabular}$\hspace{-1em}$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Mizar Mathematical Library}
\green{biggest library of formalized mathematics in the world}
\medskip

\begin{center}
\begin{tabular}{rl}
\red{44,711} & \red{lemmas} \\
\adviwait
1,660,695 & lines of `code' \\
\adviwait
58.8 & megabytes \\
\noalign{\medskip}
\adviwait
\red{152} & \red{`authors'} \\
\adviwait
834 & `articles'
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the axioms of Mizar}
\vbox to 0pt{
\vspace{-1.5\bigskipamount}
\begin{center}
\footnotesize
\begin{tabular}{lcc}
\texttt{TARSKI:def 3} && $\red{X \subseteq Y} \Iff (\forall x.\; x \in X \Implies x \in Y)$ \\
\texttt{TARSKI:def 5} && $\red{\langle x,y\rangle} = \{\{x,y\},\{x\}\}$ \\
\texttt{TARSKI:def 6} && $\red{X \sim Y} \Iff \exists Z.\, (\forall x.\, x \in X. \!\Implies\! \exists y.\, y \in Y \land \langle x,y\rangle \in Z) \land {}$ \\
&& $\phantom{X \sim Y \Iff \exists Z.\,} (\forall y.\, y \in Y. \!\Implies\! \exists x.\, x \in X \land \langle x,y\rangle \in Z) \land {}$ \\
&& $(\forall x \forall y \forall z \forall u.\, \langle x,y\rangle \in Z \land \langle z,u\rangle \in Z \Implies (x = z \Iff y = u))$ \\
\noalign{\vspace{-.1em}\color{slideblue}\rule{\linewidth}{0.04em}\vspace{.2em}}%
\texttt{TARSKI:def 1} && $x \in \red{\{y\}} \Iff x = y$ \\
\texttt{TARSKI:def 2} && $x \in \red{\{y,z\}} \Iff x = y \,\lor\, x = z$ \\
\texttt{TARSKI:def 4} && $x \in \red{\bigcup X} \Iff \exists Y.\; x \in Y \,\land\, Y \in X$ \\
\noalign{\medskip}
\texttt{TARSKI:2} && $(\forall x.\; x\in X \!\Iff\! x\in Y) \Implies X = Y$ \\
\texttt{TARSKI:7} && $x \in X \Implies \exists Y.\; Y \in X \land \neg\exists x.\; x \in X \land x \in Y$ \\
\green{\texttt{TARSKI:sch 1}} && \green{$(\forall x\,\forall y\,\forall z.\, P[x,y] \land P[x,z] \!\Implies\! y = z) \rlap{${} \Implies {}$}$} \\
&& \green{$(\exists X.\; \forall x.\; x \in X \Iff \exists y.\; y \in A \,\land\, P[y,x])$} \\
\texttt{TARSKI:9} && $\exists M.\, N\in M \land (\forall X\forall Y.\, X \in M \land Y \subseteq X \!\Implies\! Y \in M) \land {}$ \\
&& $(\forall X.\, X \in M \!\Implies\! \exists Z.\, Z \in M \land \forall Y.\, Y \subseteq X \!\Implies\! Y \in Z) \land {}$ \\
&& $(\forall X.\, X \subseteq M \!\Implies\! X \sim M \lor X \in M)$
\end{tabular}
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof: \textbf{interactively}}
\bigskip

\begin{center}
\large
\gray{DEMO}
\end{center}
\vspace{4\bigskipamount}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{utopia}
\slidetitle{`when things changed'}
\green{the three phases in the development of mathematics}
\smallskip

\begin{itemize}
%\item[$\bullet$]
%\textbf{calculation}
%
%Egyptian-Babylonian-Chinese

\item[$\bullet$]
\textbf{proof}

Greece,
fourth century BC

\item[$\bullet$]
\textbf{rigor}

nineteenth century

\item[$\bullet$]
\textbf{computer checked proof}

\red{the present}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the QED manifesto}
Boyer e.a. \\
\green{anonymous manifesto}

\begin{center}
\bigskip
\red{let's proof check all of mathematics\exclspace!}
\bigskip
\bigskip
\end{center}

very nice and thought-provoking document \\
but: nobody started \textbf{doing} anything

\begin{center}
\bigskip
\red{why\exclspace?}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why mathematicians are not interested (yet)}
\begin{itemize}
\item[$\bullet$]
\textbf{it is much too much work}

\red{one work-week for one page from an undergraduate math textbook}
\medskip

\item[$\bullet$]
\textbf{it does not have any good application}

all you get is a big tar file
\medskip

\item[$\bullet$]
\textbf{it does not resemble mathematics}

it looks like program code instead of mathematics

also: the \green{reformists} don't help

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the three reasons for computer proof}
\begin{itemize}
\item[$\bullet$]
\textbf{certainty}

catching all the mistakes

\medskip
\item[$\bullet$]
\textbf{clarity}

communicating mathematics in a totally clear way

\medskip
\item[$\bullet$]
\textbf{beauty}

\green{the cultural reason} \\
mathematics is a human artifact \& computers are its natural medium\toolong
\medskip

\red{{\dots} and furthermore, it's fun\exclspace!}

\end{itemize}

\vfill
\end{slide}

\end{document}