\documentclass[t]{beamer}
\usepackage{pgf,amssymb,rotating}
\usepackage[all]{xy}

\iftrue
\usefonttheme[onlymath]{serif}
\useinnertheme{rounded}

\definecolor{grayblue}{rgb}{.92,.92,.94}
\definecolor{grayred}{rgb}{1,.9,.9}

\setbeamercolor{palette primary}{use=structure,fg=black,bg=grayblue}
\setbeamercolor*{titlelike}{parent=palette primary}

\let\realtitlepage=\titlepage
\let\realframe=\frame
\let\realframetitle=\frametitle
\let\realinsertframenumber=\insertframenumber
\let\realauthor=\author
\let\realitemize=\itemize
\def\othertitlepage{\vbox to 0pt{\vspace{5.05em}\realtitlepage\vss}}
\def\titlepage{\addtocounter{framenumber}{-1}\subpdfbookmark{\ifx\titlelink\notitlelink\inserttitle\else\titlelink\fi}{Title}\global\let\titlepage=\othertitlepage\titlepage}
\def\otherframe{\global\def\itemize{\vspace{-.2em}\realitemize\parskip=.4em\itemsep=.7em}\global\def\frametitle##1{\belowpdfbookmark{\theframenumber. \ifx\linktitle\nolinktitle ##1\else\linktitle\fi}{Frame\theframenumber}\global\let\frametitle=\realframetitle\frametitle{##1}}\realframe}
\def\bookmarksoff{\let\frame=\realframe\let\insertframenumber=\relax}
\def\bookmarkson{\let\frame=\otherframe\let\insertframenumber=\realinsertframenumber}
\bookmarksoff

\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{items}{{\footnotesize $\gray{\blacktriangleright}$}}
\setbeamertemplate{frametitle}[default][center]
\setbeamerfont{frametitle}{size=\normalsize}
%\setbeamercolor{block body}{bg=blue!16.9}
\setbeamercolor{block body}{bg=grayred}
\AtBeginSection[]{\global\parskip=.8em\bookmarksoff\addtocounter{framenumber}{-1}\setbeamercolor{frametitle}{bg=grayred}\begin{frame}{\hfill\normalsize\textcolor{black!35}{\uppercase\expandafter{\romannumeral\thesection}}}\vspace{2.7em}\begin{block}{}\vspace{5pt}\center{{\scriptsize\strut}\textcolor[rgb]{.75,0,0}{\ifx\sectiontitle\nosectiontitle\insertsectionhead\else\sectiontitle\fi}{\scriptsize\strut}}\vspace{5.2pt}\end{block}\textcolor{black}\sectionframeextra\end{frame}\color{black}\setbeamercolor{frametitle}{bg=grayblue}\bookmarkson}
\let\sectionframeextra=\relax
\let\Tiny=\tiny

\makeatletter
\def\author#1{\let\KV@Hyp@pdfauthor=\relax\realauthor{#1}}
\newdimen\leftmargin
\newdimen\rightmargin
\setlength{\leftmargin}{\beamer@leftmargin}
\setlength{\rightmargin}{\beamer@rightmargin}
\setbeamertemplate{frametitle}{\nointerlineskip
\@tempdima=\textwidth \advance\@tempdima by\beamer@leftmargin\advance\@tempdima by\beamer@rightmargin
\begin{beamercolorbox}[wd=\@tempdima]{frametitle}\vbox to 3.5em{\vbox to 0pt{\vskip .3em
\strut\hfill\llap{\footnotesize\textcolor{black!35}{\insertframenumber}}\hskip .55em\strut\par\vss}\vss
\strut\hskip 2.6em\blue{\insertframetitle}\hfill\hskip 2.6em\strut\par\vskip .2em\vss}%
\end{beamercolorbox}\vspace{.1em}}
\makeatother
\fi

\def\datetimeevent#1#2#3#4{\date{\vspace{-.2em}\par#1$\,$, #2$\,$:$\,$#3\\\vspace{1em}{\scriptsize{#4}\par}}}

\def\toolong{$\hspace{-100cm}$}

\def\red{\textcolor[rgb]{1,0,0}}
\def\darkred{\textcolor[rgb]{.85,0,0}}
\def\green{\textcolor[rgb]{0,.5,0}}
\def\blue{\textcolor[rgb]{0,0,.5}}
\def\gray{\textcolor[rgb]{.5,.5,.5}}
\def\darkgray{\textcolor[rgb]{.4,.4,.4}}
\def\lightgray{\textcolor[rgb]{.8,.8,.8}}
\def\black{\textcolor[rgb]{0,0,0}}
\def\white{\textcolor[rgb]{1,1,1}}

\begin{document}

\def\titlelink{the next generation of proof assistants in ten questions}
\title{the next generation of proof assistants\only<2->{\rlap{\hspace{1pt}:}\break\darkred{ten questions}}}
\author{Freek Wiedijk}
\institute{Radboud University Nijmegen\\The Netherlands \pgfimage[width=10pt]{pics/flags/netherlands}}
\datetimeevent{2010 08 31}{16}{30}{LSFA 2010\\Natal, Brazil \pgfimage[width=10pt]{pics/flags/brazil}}

\begin{frame}
\titlepage
\end{frame}

\addtocounter{section}{-2}

\section{the state of the art}

\begin{frame}
\frametitle{some of the best current proof assistants}
\setlength{\unitlength}{.92pt}
\begin{picture}(0,180)(-110,-9)
\put(-16,160){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(0,160){\makebox(0,0)[l]{\strut ACL2}}
\put(-16,140){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(0,140){\makebox(0,0)[l]{\strut B method}}
\put(-16,120){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(0,120){\makebox(0,0)[l]{\strut PVS}}
\only<1>{\put(-16,100){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}}
\put(0,100){\makebox(0,0)[l]{\strut \only<2->{\gray}{HOL}}}
\only<2->{
\put(26,103){\lightgray{\vector(4,1){34}}}
\put(26,100){\lightgray{\vector(1,0){46}}}
\put(26,97){\lightgray{\vector(4,-1){46}}}
\only<3->{\put(11,94){\lightgray{\vector(0,-1){8}}}}
\put(77,100){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(93,100){\makebox(0,0)[l]{\strut HOL4}}
\put(65,116){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(77,116){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(93,116){\makebox(0,0)[l]{\strut\small HOL Light}}
\put(77,85){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(93,85){\makebox(0,0)[l]{\strut\small ProofPower}}
}
\put(-28,80){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(-16,80){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/germany}}}
\put(0,80){\makebox(0,0)[l]{\strut Isabelle}}
\put(-16,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(0,60){\makebox(0,0)[l]{\strut Coq}}
\only<4->{
\put(23,60){\lightgray{\vector(4,0){37}}}
\put(23,57){\lightgray{\vector(4,-1){49}}}
\put(65,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(77,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(93,60){\makebox(0,0)[l]{\strut\small ssreflect}}
\put(77,45){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/italy}}}
\put(93,45){\makebox(0,0)[l]{\strut\small Matita}}
}
\put(-16,40){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/poland}}}
\put(0,40){\makebox(0,0)[l]{\strut Mizar}}
\put(-16,20){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(0,20){\makebox(0,0)[l]{\strut Twelf}}
\put(-16,0){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(0,0){\makebox(0,0)[l]{\strut\small Metamath}}
\only<5->{
\put(-110,160){\makebox(0,0)[l]{{\Large $+$}}}
\only<9->{
\put(-110,140){\makebox(0,0)[l]{\darkgray{\Large $+$}}}
\put(-110,120){\makebox(0,0)[l]{\darkgray{\Large $+$}}}
}
\put(-110,100){\makebox(0,0)[l]{{\Large $+$}}}
\put(-110,80){\makebox(0,0)[l]{{\Large $+$}}}
\put(-110,60){\makebox(0,0)[l]{{\Large $+$}}}
\put(-106,-12){\makebox(0,0){\begin{rotate}{-90}\scriptsize\only<-7>{{ITP 2010}}\only<8->{\darkgray{computers}}\end{rotate}}}
}
\only<6->{
\put(-90,80){\makebox(0,0)[l]{{\Large $+$}}}
\put(-90,60){\makebox(0,0)[l]{{\Large $+$}}}
\put(-90,20){\makebox(0,0)[l]{{\Large $+$}}}
\put(-86,-12){\makebox(0,0){\begin{rotate}{-90}\scriptsize\only<-7>{{POPLmark}}\only<8->{\darkgray{logic}}\end{rotate}}}
}
\only<7->{
\put(-70,100){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,80){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,60){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,40){\makebox(0,0)[l]{{\Large $+$}}}
\only<10>{
\put(-70,0){\makebox(0,0)[l]{\darkgray{\Large $+$}}}
}
\put(-66,-12){\makebox(0,0){\begin{rotate}{-90}\scriptsize\only<-7>{{100 theorems}}\only<8->{\darkgray{mathematics}}\end{rotate}}}
}
\end{picture}

\end{frame}

\begin{frame}
\frametitle{the computer science spectrum of formal proof}
\begingroup
\vspace{-.6em}
\footnotesize
$$
\hspace{-4em}\begin{array}{c}
\uncover<12->{\mbox{non-user level programs\rlap{ \gray{like \only<13->{\green}{computer games}}}} \\}
\uncover<11->{\mbox{user level programs\rlap{ \gray{like word processors and web browsers}}} \\}
\uncover<10->{\mbox{{programmer level programs}\rlap{ \gray{like compilers and databases engines}}} \\
\darkgray{\uparrow} \\}
\uncover<9->{\mbox{\only<16->{\red}{system level programs}\rlap{ \gray{\only<16->{\red}{like operating systems} and device drivers}}} \\
\only<-15>{\darkgray}{\only<16->{\red}{\uparrow}} \\}
\uncover<8->{\mbox{high level programming languages\rlap{ \gray{like Haskell}}} \\}
\uncover<7->{\mbox{\only<15->{\red}{low level programming languages}\rlap{ \only<-14>{\gray}{\only<15->{\red}{like C}}}} \\}
\uncover<6->{\mbox{assembly programming languages} \\
\only<-14,16>{\darkgray}{\only<15,17>{\red}{\uparrow}} \\}
\uncover<5->{\mbox{\only<14-15,17>{\red}{machine code}} \\
\only<-13,15->{\darkgray}{\only<14,17>{\red}{\uparrow}} \\}
\uncover<4->{\mbox{\only<14,17>{\red}{circuits}\rlap{ specified on the register transfer level \gray{like in Verilog}}} \\
\darkgray{\uparrow} \\}
\uncover<3->{\mbox{circuits\rlap{ made of logical gates \gray{as described in a netlist}}} \\
\darkgray{\uparrow} \\}
\uncover<2->{\mbox{circuits\rlap{ made of electronic components \gray{like \only<13->{\green}{transistors}}}}}
%\mbox{electrons\rlap{ moving through substrates \gray{like doped silicon}}}
\end{array}\hspace{14em}
$$
\endgroup
\end{frame}

\begin{frame}
\frametitle{formally proving a processor correct}
\vbox to 0pt{
\vspace{2em}
\begingroup
\setlength\tabcolsep{0pt}
\begin{tabular}{cc}
\pgfimage[width=14em]{pics/arm1} &
\pgfimage[width=14em]{pics/arm2} \\
\noalign{\bigskip}
{\small ARM}6 architecture & {\small ARM}v3 instruction set
\end{tabular}
\endgroup
\vss}
\vspace{-1.25em}
Anthony Fox, HOL4, \pgfimage[width=10pt]{pics/flags/uk}\ University of Cambridge, 2002
\end{frame}

\begin{frame}
\frametitle{formally proving a compiler correct}
\vbox to 0pt{
\vspace{0em}
\hspace{2em}\pgfimage[width=24em]{pics/compcert}
\vss}
\vspace{-1.25em}
Xavier Leroy, Coq, \pgfimage[width=10pt]{pics/flags/france}\ INRIA, 2006
\end{frame}

\begin{frame}
\frametitle{formally proving an operating system correct}
Gerwin Klein, Isabelle, \pgfimage[width=10pt]{pics/flags/australia}\ NICTA, 2009

\blue{L4.verified project = verification of seL4 microkernel}

\begin{center}
\setlength{\tabcolsep}{0em}
\begin{tabular}{rl}
\green{1} \strut & \green{microkernel} \\
\green{\only<4>{\red}{8,700}} \strut & \green{\only<4>{\red}{lines of C}} \\
\green{0} \strut & \green{bugs$\hspace{.5pt}^{*}$} \\
\noalign{\vspace{.7em}}
& \green{qed} \\
\noalign{\vspace{2.2em}}
\uncover<2->{5,700 \strut & lines of Haskell} \\
\noalign{\vspace{.7em}}
\uncover<3->{117,000 \strut & lines of Isabelle \\
\only<4>{\red}{20} \strut & \only<4>{\red}{person-years}}
\end{tabular}\hspace{6em}\strut
\end{center}
\begin{flushright}
\vspace{-7.7em}
\footnotesize\green{{$^{*}$\hspace{.5pt}conditions apply}}\hspace{4em}\strut
\end{flushright}
\end{frame}

\begin{frame}
\frametitle{the mathematics spectrum of formal proof}
\begingroup
\vspace{-.6em}
\footnotesize
$$
\hspace{-100em}%
\setlength{\arraycolsep}{1em}%
\lightgray{\begin{array}{cl}
\uncover<12->{\mbox{\black{proofs {that are a large team effort}}} &
\mbox{{\green{\only<12>{\red}{classification of finite simple groups}}}} \\
\noalign{\smallskip}
\darkgray{\uparrow} &
\mbox{\uncover<14->{\green{\only<14>{\red}{Fermat's last theorem}}}}} \\
\noalign{\smallskip}
\uncover<10->{\mbox{\black{recent solutions to famous open problems}} &
\mbox{\uncover<11->{\green{\only<11,17>{\red}{$\mbox{P} \ne \mbox{NP}$?}}}} \\
\noalign{\smallskip}
\darkgray{\uparrow} &
\mbox{\uncover<13->{\green{\only<13,17>{\red}{{Kepler conjecture}}}}}}
\only<-15>{\\ \noalign{\smallskip}}
\only<16->{\\ \noalign{\medskip}
\hline
\noalign{\medskip}}
\uncover<9->{\mbox{\black{proofs with large computer calculations}} &
\mbox{\green{\only<19>{\red}{four color theorem}}} \\}
\uncover<6,9->{\only<6>{\mbox{\black{research mathematics}}}\only<9->{\darkgray{\uparrow}}} \\
\uncover<6->{\only<6>{\darkgray{\uparrow}}\only<7->{\mbox{\black{\only<17>{\red}{\only<18->{\lightgray}{research mathematics}}}}}} \\
\uncover<5->{\mbox{\black{graduate mathematics}} &
\mbox{\uncover<8->{\green{\only<19->{\red}{prime number theorem}}}} \\
\darkgray{\uparrow} &
\mbox{\uncover<8->{\green{Jordan curve theorem}}} \\}
\uncover<4->{\mbox{\black{undergraduate mathematics}} &
\mbox{\uncover<8->{\green{fundamental theorem of algebra}}} \\
\darkgray{\uparrow} \\}
\uncover<3->{\mbox{\black{high school mathematics}} &
\mbox{\gray{= basic algebra and calculus}} \\
\darkgray{\uparrow} \\}
\uncover<2->{\mbox{\black{elementary school mathematics}} &
\mbox{\gray{= arithmetic}}}
\end{array}\hspace{-101em}}
$$
\endgroup
\end{frame}

\begin{frame}[fragile]
\frametitle{formally proving the prime number theorem}
John Harrison, HOL Light, \pgfimage[width=10pt]{pics/flags/usa}\ Intel, 2008
\vspace{-.5em}

$$\green{2\pi i F(w) = \int_{\red{\Gamma}} F(z + w) N^z \left(\frac{1}{z} + \frac{z}{R^2}\!\right) dz}$$
\begin{center}
\vspace{-0em}
\red{\begin{picture}(40,40)
\put(20,20){\circle{40}}
\put(-10,-5){\white{\rule{30pt}{50pt}}}
\put(-10,20){\gray{\line(1,0){60}}}
\put(20,-10){\gray{\line(0,1){60}}}
\put(20,20){\gray{\circle*{2.2}}}
\put(15,0){\line(1,0){5}}
\put(15,40){\line(0,-1){40}}
\put(15,40){\line(1,0){5}}
\put(20,0){{\circle*{2.2}}}
\put(20,40){{\circle*{2.2}}}
\end{picture}}\hspace{4em}\strut
\end{center}
\vbox to 0pt{
\vspace{-4.5em}
\begingroup
\def\\{\char`\\}
\begin{semiverbatim}\footnotesize
  \gray{\textsf{\normalsize\textsl{etcetera}}}\vspace{.5\smallskipamount}
  ALL_TAC] THEN
SUBGOAL_THEN
 `\green{((\\z. f(w + z) * Cx(&N) cpow z * (Cx(&1) / z + z / Cx(R) pow 2))\toolong
  has_path_integral (Cx(&2) * Cx pi * ii * f(w))) (\red{A ++ B})}`
ASSUME_TAC THENL
 [MP_TAC(ISPECL\vspace{.5\smallskipamount}
  \gray{\textsf{\normalsize\textsl{etcetera}}}
\end{semiverbatim}
\endgroup
\vss}
\end{frame}

\begin{frame}
\frametitle{formally proving the four color theorem}
Georges Gonthier, Coq/ssreflect, \pgfimage[width=10pt]{pics/flags/uk}\ Microsoft + \pgfimage[width=10pt]{pics/flags/france}\ INRIA, 2006
\vbox to 0pt{
\vspace{-.7em}
\hfill\pgfimage[width=13em]{pics/confs}\hspace{-.3em}
\vss
}
\vspace{2.2em}

\begin{itemize}
\item
Appel \& Haken, 1976 \\
\green{assembly program}

\item
Robertson, Sanders, Seymour \& Thomas, 1997 \\
\green{C program}

\item
Gonthier \\ \green{purely functional \gray{(= no state)} \only<2>{\gray}{OCaml}\only<2>{\gray{$\,\to\,$}\red{Coq}} program}

\end{itemize}

\end{frame}

\section{proof assistants: the next generation}

\begin{frame}[fragile]
\frametitle{an email from Tobias Nipkow}

\vbox to 0pt{
\begin{picture}(0,0)
\uncover<2->{\put(250,-67){\green{\vector(-3,-2){20}}}
\put(253,-65){\makebox(0,0)[bl]{\green{\small me}}}}
\uncover<3->{\put(247,-158){\blue{\vector(-3,2){20}}}
\put(250,-160){\makebox(0,0)[tl]{\blue{\small Tobias}}}}
\end{picture}
\vss
}
\vspace{-2.1em}

\def\xdots{{\rm\footnotesize {\scriptsize [}\hspace{1.8pt}\dots{\scriptsize ]}}}
\begin{semiverbatim}\footnotesize
\gray{Message-ID: <4785C81D.2090607@in.tum.de>
Date: Thu, 10 Jan 2008 08:24:13 +0100
From: Tobias Nipkow <nipkow@in.tum.de>
To: Freek Wiedijk <freek@cs.ru.nl>
Subject: Re: [Fwd: free ultrafilters]\medskip
\xdots}\bigskip
\only<2-3>{\green}{> I personally _hate_ the totality of the HOL logic.  Don't
> you?}\medskip
\only<3>{\blue}{Occasionally I do. But mostly not.\medskip
The \only<4>{\red}{next generation of proof assistants} will take it into account.}\toolong\bigskip
\gray{\xdots}
\end{semiverbatim}

\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break be based on ZFC set theory?}
\def\sectionframeextra{
\only<2->{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\only<3->{\lightgray}{ACL2} \\
\only<4->{\gray}{B method} \\
\only<3->{\lightgray}{PVS} \\
\only<3->{\lightgray}{HOL} \\
$\hspace{-2em}${\only<5>{\gray}{Isabelle}}\only<5>{{/ZF}}$\hspace{-2em}$ \\
\only<3->{\lightgray}{Coq} \\
{Mizar} \\
\only<3->{\lightgray}{Twelf} \\
{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{I. should ... be based on ZFC set theory?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{foundations for proof assistants}
\begin{itemize}
\item
\textbf{set theory} \gray{\small (Mizar, Isabelle/ZF, Metamath, B method)} \\
\red{Zermelo-Fraenkel axioms + axiom of Choice} \\\vspace{1pt}
\uncover<2->{\small\green{untyped, not computational, classical, canonical}}

\item
\textbf{type theory} \gray{\small (Coq, Twelf)} \\
\normalsize\red{Curry-Howard isomorphism}\uncover<4->{, {\small predicative? intensional?}}\normalsize\strut\\\vspace{1pt}
\uncover<3->{\small\green{typed, computational, intuitionistic, many variations} \\
\uncover<7->{\small\green{as expressive as set theory}}}

\item
\textbf{higher order logic} \gray{\small (HOL, Isabelle/HOL, PVS)} \\\vspace{1pt}
\uncover<5->{\small\green{typed, not computational, classical, canonical}} \\
\uncover<8->{\small\green{less expressive}}

\item
\textbf{primitive recursive arithmetic} \gray{\small (ACL2)} \\\vspace{1pt}
\uncover<6->{\small\green{untyped, computational, classical, canonical} \\
\uncover<9->{\small\green{even less expressive}}}

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{first order logic versus higher order logic}
\green{`canonical logic'} = classical first order predicate logic with equality 
\pause

$$
\begin{array}{c}
\mbox{\green{first order logic}} \\
\cap \\
\mbox{\red{higher order logic}} \\
\cap \\
\mbox{\green{first order logic}} + \only<3->{\mbox{\red{\textbf{schemes}}} +} \mbox{set theory}
\end{array}
\pause
\pause
$$

\vspace{-.5em}
\red{\textbf{binders}}
$${\{ x \in A \mathrel{|} P(x) \}}$$
$${\textstyle\sum_{i=1}^n a_i}$$
$${\textstyle\lim_{x\to a} f(x)}$$
$${\textstyle\int f(x)dx}$$

\end{frame}

\iffalse
\begin{frame}
\frametitle{does computation belong in the foundations?}
{requirement:} proof checking \green{should be linear time}

\textsl{checking a proof by following it with your little finger}
\vspace{1.5em}
\pause

proof checking in type theory is \red{non-elementary}
$$\mbox{\red{infeasible}} \approx \mbox{\red{undecidable in practice}}
\vspace{1.5em}
\pause
$$
\textsl{\red{`left as an exercise to the reader'}} is in itself not a \green{proof}\pause \\
\darkgray{\dots\ even if the method to solve the exercise is algorithmic\pause}
\begin{eqnarray*}
\mbox{\red{program to generate a proof}} &\ne& \mbox{\green{output of that program}} \\
\mbox{\red{proof script}} &\ne& \mbox{\green{proof object}}
\end{eqnarray*}

\end{frame}
\fi

\def\sectiontitle{should the next generation of proof assistants\break have an advanced type system?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\lightgray{ACL2} \\
\lightgray{B method} \\
{PVS} \\
\lightgray{HOL} \\
\lightgray{Isabelle} \\
{Coq} \\
{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{II. should ... have an advanced type system?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{soft types}
\begin{itemize}
\item
\textbf{no types} \gray{\small (Metamath)}

\item
\textbf{hard types} \gray{\small (PVS, HOL, Isabelle, Coq, Twelf)} \\
\green{types are part of the foundation}

\item
\textbf{soft types} \gray{\small (ACL2, B method, Mizar)} \\
\green{types are a layer on top of an untyped foundation}
\medskip
\pause

\red{`types as predicates'} \\
{type inference = automated predicate proving}
\begin{eqnarray*}
\forall x \red{{} : A\only<3->{\blue{(y, \dots}\blue{)}}}.\, P(x) &\mbox{is syntax for}& \forall x.\, \red{{A(x\only<3->{\blue{,y,\dots}})} \Rightarrow{}} P(x)\only<3->{\hspace{3.7pt}}
\pause
\end{eqnarray*}
natural interpretation for \blue{dependent types} \\\pause
{no} natural interpretation for \blue{function types} \red{$A\to B$}
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{dependent types and empty types}
\begin{itemize}
\item
\textbf{dependent types}
\begin{center}\small
\green{
\only<4>{\red}{element of a given set} \\
element of a \only<2>{\red}{given algebraic structure} \\
array of a given length \\
\only<3>{\red}{normal form of a given lambda term} \\
vector space of a given dimension \\
field extension of a given field by a given degree\pause
\medskip
}
\end{center}
essential for \only<2>{\red}{implicit arguments} in notations \\
$x + y$\enskip for\enskip $x +_{\only<2>{\red}{G}} y$\enskip when\enskip $x, y$ are elements of a group ${\only<2>{\red}{G}}$\smallskip\pause

\item
\textbf{empty types}

\only<3>{\red}{unavoidable} with natural definitions of dependent types
\vspace{-.5em}
\pause

\uncover<4>{$$\blue{\mbox{\red{set}} \;\hookrightarrow\; \mbox{{class}} \;\leftrightarrow\; \mbox{\red{type}}}$$}

\end{itemize}

\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break take partiality seriously?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
{ACL2} \\
{B method} \\
{PVS} \\
\lightgray{HOL} \\
\lightgray{Isabelle} \\
\lightgray{Coq} \\
\lightgray{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{III. should ... take partiality seriously?}
\def\sectionframeextra{}

\begin{frame}
\def\linktitle{the value of 1/0}
\frametitle{the value of $\displaystyle\frac{1}{0}$}
\begin{itemize}
\item
\textbf{$\displaystyle\frac{1}{0} = 0$ is provable} \gray{\small (ACL2, HOL, Isabelle/HOL, Mizar)}

\item
\textbf{$\displaystyle\frac{1}{0} = 0$ is disprovable} \gray{\small (Metamath\only<2->{, \only<2-4>{\green}{IMPS}})}
\small
\vspace{-.9em}
$$\uncover<2->{\mbox{\gray{\only<2-4>{\green}{{proof$\,$}}} $\displaystyle\frac{1}{0}$ is undefined, $0$ is defined \gray{\only<2-4>{\green}{$\,${qed}}}}}\vspace{-1em}$$
$$\uncover<3->{{\frac{1}{0} \mathrel{\setbox0\hbox{{=}}\hbox to\wd0{\hss\only<4>{\red}{\only<4>{\textbf}{=}}}} \frac{1}{0}\;\mbox{\gray{\only<3-4>{\green}{\large ?}}}}}\vspace{-2.2em}$$
\normalsize
%
\item
\textbf{$\displaystyle\frac{1}{0} = 0$ is neither provable nor disprovable} \gray{\small (Coq)}

\item
\textbf{$\displaystyle\frac{1}{0} = 0$ is illegal} \gray{\small (\only<8>{\red}{ACL2/gold, B method, PVS}, \only<5-6>{\green}{Coq/CoRN, Twelf})}
\pause\pause\pause\pause
\vspace{-.5em}
\small

$$\only<7->{\gray}{\frac{1}{\only<5>{\red{x}}\only<6->{0}} = \only<5>{\red{y}}\only<6->{0}}$$
$$\setbox0\hbox{$0$}{\mbox{div}(1,\hbox to\wd0{\hss$\only<5>{\red{x}}\only<6->{0}$\hss},{\only<-6>{\green}{\langle\mbox{\small\textsl{proof object for\hspace{.5pt} $\hbox to\wd0{\hss$\only<5>{\red{x}}\only<6->{0}$\hss} \ne 0$}}\rangle}}) = \hbox to\wd0{\hss$\only<5>{\red{y}}\only<6->{0}$\hss}}$$

\end{itemize}
\end{frame}

\begin{frame}
\frametitle{definedness conditions}
each function $f(x_1,\dots,x_n)$ has a \blue{domain predicate} $D_f(x_1,\dots,x_n)$\toolong
$$\blue{D_{\sf div}}(x,y) \Leftrightarrow (y \ne 0)$$
each formula $\phi$ has a \blue{definedness condition} $\Delta(\phi)$
$$\blue{\Delta}(\frac{1}{0} = 0) \Leftrightarrow D_{\sf div}(1,0) \Leftrightarrow (0 \ne 0) \Leftrightarrow \bot\vspace{-1.2em}\pause$$
$$\blue{\Delta}({\only<2-4>{\red}{\mbox{\large $\forall$} x \in {\mathbb R}.\;x\ne 0 \Rightarrow \frac{1}{x}\ne 0})}\;\mbox{\large \uncover<2>{{?}}}\vspace{-.7em}\pause$$
$$\green{\Delta(\phi \Rightarrow \psi) \Leftrightarrow (\Delta(\phi) \land (\phi \Rightarrow \Delta(\psi)))\pause}$$
$$\green{\Delta(\phi \land \psi) \Leftrightarrow (\Delta(\phi) \land (\phi \Rightarrow \Delta(\psi)))}\medskip\pause$$
{$\Delta$ does \red{not} respect logical equivalence}
$$\green{{\Delta(\phi \land \psi)} \mathrel{\red{\;\not\!\Leftrightarrow}} \green{\Delta(\psi \land \phi)}}$$

\end{frame}

\iffalse
\begin{frame}
\frametitle{a library of formal proofs for the future}
current libraries of formal mathematics use strange definitions
$$\green{\frac{1}{0}\mbox{ is a real number \gray{\small (HOL, Isabelle/HOL, Coq, Mizar, ACL2)}}}$$
\blue{\pause or else}

current libraries of formal mathematics only make sense with very idiosyncratic logical foundations
\bigskip
\pause

should we first develop a large library of formal mathematics?

\blue{or}

should we first develop the next generation of proof assistants?\\\pause
\red{canonical predicate logic with definedness conditions?}

\end{frame}
\fi

\def\sectiontitle{should the next generation of proof assistants\break take category theory seriously?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\lightgray{ACL2} \\
\lightgray{B method} \\
\lightgray{PVS} \\
\lightgray{HOL} \\
\lightgray{Isabelle} \\
{Coq} \\
{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{IV. should ... take category theory seriously?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{the snake lemma and the category of Abelian groups}
\vbox to 0pt{
$$
{\xymatrix@R=.5em@C=.6em{
& && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && & \\\\
& && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && & \\\\
& && \bullet\ar[dd]\ar[rr] && \bullet\ar[dd]\ar[rr] && \bullet\ar[dd]\ar[rr] && 0 & \\
&&&&&&&& \\
& 0\ar[rr] && \bullet\ar[rr] && \bullet\ar[rr] && \bullet && & \\\\
& && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && & \\\\
& && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && &
}}\pause
$$
\vss
}\vspace{-1.24em}
\vbox to 0pt{
$$
\gray{\xymatrix@R=.5em@C=.6em{
& && 0\ar[dd] && 0\ar[dd] && 0\ar[dd] && & \\\\
& && \bullet\ar[dd] && \bullet\ar[dd] && \bullet\ar[dd] && & \\\\
& && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$0$}} & \\
&&&&&&&& \\
& \mbox{\phantom{$0$}} && \mbox{\phantom{$\bullet$}}\ar[dd] && \mbox{\phantom{$\bullet$}}\ar[dd] && \mbox{\phantom{$\bullet$}}\ar[dd] && & \\\\
& && \bullet\ar[dd] && \bullet\ar[dd] && \bullet\ar[dd] && & \\\\
& && 0 && 0 && 0 && &
}}\pause
$$
\vss
}\vspace{-1.24em}
\vbox to 0pt{
$$
\red{\xymatrix@R=.5em@C=.6em{
& && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && & \\\\
& && \bullet\ar[rr] && \bullet\ar[rr] && \bullet\ar`r[ddrrr]`[dddr]`[ddddlllllll]`[ddddddllllll][ddddddllll] && & \\\\
& && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$0$}} & \\
&&&&&&&& \\
& \mbox{\phantom{$0$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && \mbox{\phantom{$\bullet$}} && & \\\\
& && \bullet\ar[rr] && \bullet\ar[rr] && \bullet && & \\\\
& && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && \mbox{\phantom{$0$}} && &
}}\pause
$$
\vss
}
\vspace{15.5em}

\blue{I don't like universes\hspace{.5pt}!}
\end{frame}

\begin{frame}
\frametitle{Vladimir Voevodsky and the formalization of the real numbers}
Vladimir Voevodsky, \pgfimage[width=10pt]{pics/flags/russia}\hspace{1.04pt}\pgfimage[width=10pt]{pics/flags/usa}\ Institute for Advanced Study \\
\textsl{Fields medal} in 2002
\pause

\blue{homotopy type theory, 2006}
\vspace{-1em}
\pause

\begin{flushleft}\leftskip=1.75em\rightskip=1.75em\looseness=-1
\textsl{\small I will speak about type systems.
It is difficult for a mathematician since a type system is not a mathematical notion.}
%\hfill{\small ---The equivalence axiom and univalent models of type theory}$\hspace{-2em}$%
\pause
\vspace{-1em}
\end{flushleft}

$\red{{\mathbb R} =}$
\vspace{-2em}
\begin{center}\small
set of Dedekind cuts\hspace{1pt}\red{?} \\
set of equivalence classes of Cauchy sequences\hspace{1pt}\red{?} \\\pause
set of equivalence classes of pairs of \textsl{positive} real numbers\hspace{1pt}\red{?} \\\pause
\red{any} field isomorphic to the real numbers\hspace{1pt}\red{?} \\\pause
{any} \red{set} of the cardinality of the real numbers\hspace{1pt}\red{?}\pause
\vspace{-.8em}
\end{center}
\green{abstract datatypes in mathematics\hspace{.5pt}?} \\\pause
\green{hardwire `up to isomorphism' in the logical foundations\hspace{.5pt}?}

\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break be based on a logical framework?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\lightgray{ACL2} \\
\lightgray{B method} \\
\lightgray{PVS} \\
\lightgray{HOL} \\
{Isabelle} \\
\lightgray{Coq} \\
\lightgray{Mizar} \\
{Twelf} \\
{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{V. should ... be based on a logical framework?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{logical frameworks}
\begin{itemize}
\item
\textbf{Twelf} = \blue{LF} \\
\green{minimal type theory}

\item
\textbf{Isabelle}/Pure \\
\green{minimal higher order logic}

\item
\textbf{Metamath} \\
\green{minimal string manipulation} \\
\uncover<2->{not HOAS: not invariant under variable renaming}

\uncover<3->{\item
\textbf{Automath} = AUT-SL = \blue{$\Delta\Lambda$} \\
\blue{N.G. de Bruijn, \pgfimage[width=10pt]{pics/flags/netherlands}\ Eindhoven University of Technology, 1987}
\green{very similar to LF but more elegant} \\
%purest HOAS: no distinction between $\lambda x{:}A.B$ and $\Pi x{:}A.B$ \\
}

\uncover<4>{\item
\blue{$\Delta\Lambda$} with a \textbf{bounded conversion rule}\hspace{.5pt}?}

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{reasons for using a logical framework}
\begin{itemize}
\item
\only<2->{\gray}{\textbf{varying the logic} \\
taking G\"odel's incompleteness theorem seriously \\
tracking what is used in a proof}
\begin{center}\small\green{\only<2->{\gray}{%
classical logic\hspace{.5pt}? \\
K axiom about equality of equality proofs\hspace{.5pt}? \\
axiom of choice\hspace{.5pt}? \\
large cardinal axioms\hspace{.5pt}? \\
Hilbert's $\epsilon$ choice operator\hspace{.5pt}? \\
universes\hspace{.5pt}?
}}
\pause
\end{center}

\item
\textbf{simplifying the logical kernel} \\
\red{DNA of formal mathematics}
\pause
\medskip

\red{$\Delta\Lambda$ `term'} =
directed graph with four kinds of nodes \\
\green{out-degrees: 2, 2, 1, 0}

\end{itemize}
\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break have a self-verified kernel?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
{ACL2} \\
\lightgray{B method} \\
\lightgray{PVS} \\
{HOL} \\
\lightgray{Isabelle} \\
{Coq} \\
\lightgray{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{VI. should ... have a self-verified kernel?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{state of the art in self-verification}
\begin{itemize}
\item
\textbf{Coq in Coq} = \textbf{Coc} \\
Bruno Barras, \pgfimage[width=10pt]{pics/flags/france}\ Universit\'e Paris 7, 1999

version of Coq kernel as a Coq program, extracted to OCaml \\
\green{not close to Coq source, can check proofs from real Coq}
\pause

\item
\textbf{HOL in HOL} \\
John Harrison, \pgfimage[width=10pt]{pics/flags/usa}\ Intel, 2006

simplified HOL kernel as a HOL program \\
\green{very close to HOL source, cannot check HOL proofs}
\pause

\item
\textbf{ACL2 in ACL2} = \textbf{Milawa} \\
Jared Davis, \pgfimage[width=10pt]{pics/flags/usa}\ University of Texas, 2009

various approximations to ACL2 as an ACL2 program \\
\green{not close to ACL2 source, can check proofs from real ACL2}

\end{itemize}
\end{frame}

\begin{frame}
\frametitle{the philosophy of certainty}
\begin{itemize}
\item
\blue{reliability of hardware and software infrastructure\hspace{.5pt}?}
\pause

\item
\blue{how can a system validate itself\hspace{.5pt}?}

{if it is incorrect it can falsely claim to be correct}
\pause

\item
\blue{G\"odel's second incompleteness theorem\hspace{.5pt}?} \\
\red{no consistent logical system can prove its own consistency}
\medskip
\pause

not: \textbf{system cannot prove false} \\
but: \textbf{system implements logic}
\bigskip
\pause

just one additional line
$$\green{\mbox{\qquad\uncover<5>{{logic cannot prove false}}\only<7>{\llap{\textbf{inaccessible cardinal axiom}}}\only<6>{\llap{logic has a model}}} \,\vdash \mbox{system cannot prove false}}$$


\end{itemize}

\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break be programmed in itself?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
{ACL2} \\
\lightgray{B method} \\
\lightgray{PVS} \\
\lightgray{HOL} \\
{Isabelle} \\
{Coq} \\
\lightgray{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{VII. should ... be programmed in itself?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{languages in proof assistants}
\begin{itemize}
\item
\textbf{implementation language} \\
\green{language the implementer uses to implement the system}

\uncover<5->{Coq: \blue{OCaml}}
\pause

\item
\textbf{scripting language} \\
\green{language the user uses to automate proofs in the system}

\uncover<6->{Coq: \blue{Ltac}}
\pause

\item
\textbf{mathematical language} \\
\green{language the user uses to write mathematics}
\only<4->{\\ \green{\dots\;and mathematical algorithms}}

\uncover<7->{Coq: \blue{Gallina}}\uncover<9>{\blue{, {Program}}}
\pause\pause\pause\pause\pause

\end{itemize}
\red{OCaml, Ltac, Gallina\only<9>{, Program}: \only<-8>{three very}\only<9>{\textsl{four}} similar programming languages}\toolong

\end{frame}

\begin{frame}
\frametitle{programming language versus mathematical language}
\begin{itemize}
\item
\textbf{type theory:}
$$
\begin{array}{c}
\noalign{\smallskip}
\mbox{mathematical language} \\
\cap \\
\mbox{programming language}
\end{array}
\smallskip
$$

\green{mathematical functions = \textsl{terminating} programs}
\pause

\item
\textbf{better:}
$$
\begin{array}{c}
\noalign{\smallskip}
\mbox{programming language} \\
\cap \\
\mbox{mathematical language}
\end{array}
\smallskip
$$

\green{programs = \textsl{executable} function definitions}

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{the mathematical function versus the executable object}
all actual computers are finite state machines
\pause

\begin{center}
\begin{picture}(0,0)(0,-32)
\put(0,-26){\makebox(0,0){\blue{\texttt{\footnotesize let rec \red{fac n} = if n=0 then 1 else n*(fac(n-1));;}}}}
\pause
\put(-20,-34){\darkgray{\vector(-1,-1){19}}}
\put(-80,-60){\makebox(0,0){\green{\strut mathematical function}}}
\put(-80,-94){\makebox(0,0){\green{\large \&}}}
\put(-80,-110){\makebox(0,0){\green{\strut \textsl{theorem} about}}}
\put(-80,-123){\makebox(0,0){\green{\strut the definition of the}}}
\put(-80,-136){\makebox(0,0){\green{\strut mathematical function}}}
\put(-80,-77){\makebox(0,0){${\sf fac} : {\mathbb Z}_{{}\ge 0} \to {\mathbb Z}$}}
\pause
\put(20,-34){\darkgray{\vector(1,-1){19}}}
\put(80,-60){\makebox(0,0){\green{\strut executable object}}}
\put(52,-73){\makebox(0,0)[tl]{\scriptsize\tt\ 2\;\ ACC0}}
\put(52,-81){\makebox(0,0)[tl]{\scriptsize\tt\ 3\;\ BNEQ 0, 9}}
\put(52,-89){\makebox(0,0)[tl]{\scriptsize\tt\ 6\;\ CONST1}}
\put(52,-97){\makebox(0,0)[tl]{\scriptsize\tt\ 7\;\ RETURN 1}}
\put(52,-105){\makebox(0,0)[tl]{\scriptsize\tt\ 9\;\ ACC0}}
\put(52,-113){\makebox(0,0)[tl]{\scriptsize\tt 10\;\ OFFSETINT -1}}
\put(52,-121){\makebox(0,0)[tl]{\scriptsize\tt 12\;\ PUSHOFFSETCLOSURE0}}
\put(52,-129){\makebox(0,0)[tl]{\scriptsize\tt 13\;\ APPLY1}}
\put(52,-137){\makebox(0,0)[tl]{\scriptsize\tt 14\;\ PUSHACC1}}
\put(52,-145){\makebox(0,0)[tl]{\scriptsize\tt 15\;\ MULINT}}
\put(52,-153){\makebox(0,0)[tl]{\scriptsize\tt 16\;\ RETURN 1}}
\pause
\put(0,-34){\darkgray{\vector(0,-1){137}}}
\put(0,-180){\makebox(0,0){\green{\strut \textsl{theorem} about the relation between the two}}}
\end{picture}
\end{center}
\end{frame}

\iffalse
\begin{frame}
\frametitle{computer science versus mathematics?}
\setlength{\unitlength}{.92pt}
\begin{picture}(0,140)(-110,-9)
\put(-16,120){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(0,120){\makebox(0,0)[l]{\strut PVS}}
\put(0,100){\makebox(0,0)[l]{\strut\gray{HOL}}}
\put(26,103){\lightgray{\vector(4,1){34}}}
\put(26,100){\lightgray{\vector(1,0){46}}}
\put(26,97){\lightgray{\vector(4,-1){46}}}
\put(11,94){\lightgray{\vector(0,-1){8}}}
\put(77,100){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(93,100){\makebox(0,0)[l]{\strut HOL4}}
\put(65,116){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(77,116){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/usa}}}
\put(93,116){\makebox(0,0)[l]{\strut\small HOL Light}}
\put(77,85){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(93,85){\makebox(0,0)[l]{\strut\small ProofPower}}
\put(-28,80){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(-16,80){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/germany}}}
\put(0,80){\makebox(0,0)[l]{\strut Isabelle}}
\put(-16,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(0,60){\makebox(0,0)[l]{\strut Coq}}
\put(23,60){\lightgray{\vector(4,0){37}}}
\put(23,57){\lightgray{\vector(4,-1){49}}}
\put(65,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(77,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(93,60){\makebox(0,0)[l]{\strut\small ssreflect}}
\put(77,45){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/italy}}}
\put(93,45){\makebox(0,0)[l]{\strut\small Matita}}
\put(-90,120){\makebox(0,0)[l]{{\Large $+$}}}
\put(-90,100){\makebox(0,0)[l]{{\Large $+$}}}
\put(-90,80){\makebox(0,0)[l]{{\Large $+$}}}
\put(-90,60){\makebox(0,0)[l]{{\Large $+$}}}
\put(-86,45){\makebox(0,0){\begin{rotate}{-90}\scriptsize{{computers}}\end{rotate}}}
\put(-70,120){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,100){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,80){\makebox(0,0)[l]{{\Large $+$}}}
\put(-70,60){\makebox(0,0)[l]{{\Large $+$}}}
\put(-66,45){\makebox(0,0){\begin{rotate}{-90}\scriptsize{{mathematics}}\end{rotate}}}
\end{picture}
\pause
\bigskip

\green{a single system for program verification \textsl{and} for mathematics?}

\end{frame}
\fi

\def\sectiontitle{should the next generation of proof assistants\break be competitive with commercial computer algebra?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\lightgray{ACL2} \\
\lightgray{B method} \\
{PVS} \\
{HOL} \\
{Isabelle} \\
{Coq} \\
\lightgray{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{VIII. should ... be competitive with commercial computer algebra?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{the reliability of computer algebra systems}
\texttt{\small > \green{\only<1-2>{\red}{\only<3>{\gray}{2*infinity-infinity}\only<1-2>{;}}\only<3->{\gray{,}{ 2*x-x;}}}}\pause
$$\mbox{\only<3>{\gray}{undefined}\pause\only<3->{\only<3>{\gray}{,} $x$}}$$
\texttt{\pause\small > \green{subs(x=infinity, 2*x-x);}}
$${\sf infinity}$$
\texttt{\pause\small > \green{{{\only<6->{\only<6>{\red}{int(}}{1/(1-x)\only<6->{\only<6>{\red}{,x)}} = }\only<6->{\only<6>{\red}{int(}}\only<5>{\red}{simplify(}{1/(1-x)}\only<5>{\red}{)}\only<6->{\only<6>{\red}{,x)}{;}}}}}}
$$\only<5>{{\frac{1}{1 - x} = -\frac{1}{-1 + x}}}\pause$$
{\vspace{-3.1em}}
$$-\ln(1 - x) = -\ln(-1 + x)\medskip$$
\texttt{\pause\small > \green{evalf(subs(x=-1, \char`\%));}}
$$-0.6931471806 = -0.6931471806 - 3.141592654 i\vspace{-100cm}$$

\end{frame}

\iffalse
\begin{frame}
\frametitle{automation in proof assistants}
\begin{itemize}
\item
\blue{decision procedures}

fast, dependable, restricted application domain

\item
\blue{generic proof search}

slow, unpredictable, often does not work
\pause

\item
\blue{domain specific heuristic proof search}

\only<2>{\red}{more open-ended}, \only<2>{\red}{more intelligent}\pause

\end{itemize}
$$\green{x \ne 0 \;\land\; \big|\ln |x|\big| > 2 \;\land\, \int_0^{|x|} t\, dt \le 1 \;\,\Rightarrow\;\, -\frac{1}{e^2} < x < \frac{1}{e^2}}\vspace{.8em}$$
\red{\pause computer algebra under hypotheses} \\
\only<4>{any high school student}\only<5>{proof assistants} can\only<5>{not} do this \only<5>{by themselves yet}

\end{frame}
\fi

\begin{frame}
\frametitle{killer app for proof assistants?}
\begin{itemize}
\item
reliable \textbf{software} and \textbf{hardware} development
\pause

\item
mathematics \textbf{education}

\green{teaching students about mathematical proof} \\
{Christophe Rafalli, \pgfimage[width=10pt]{pics/flags/france}\ Universit\'e de Savoie, 2002} 
\pause

\item
mathematically sound \textbf{computer algebra}
\pause

\green{performance\hspace{.5pt}? features\hspace{.5pt}?}
\bigskip
\medskip
\pause

{computers cannot do \textbf{high school mathematics} \uncover<6>{yet}}
$$\blue{x \ne 0 \;\land\; \big|\ln |x|\big| > 2 \;\land\, \int_0^{|x|} t\, dt \le 1 \;\,\Rightarrow\;\, -\frac{1}{e^2} < x < \frac{1}{e^2}}$$

\end{itemize}

\end{frame}

\def\sectiontitle{should the next generation of proof assistants\break use a declarative proof style?}
\def\sectionframeextra{
\only<2>{
\vspace{-1.2em}
\begin{flushright}\scriptsize
\begin{tabular}{c}
\lightgray{ACL2} \\
\lightgray{B method} \\
\lightgray{PVS} \\
\lightgray{HOL} \\
{Isabelle} \\
\lightgray{Coq} \\
{Mizar} \\
\lightgray{Twelf} \\
\lightgray{Metamath}
\end{tabular}
\end{flushright}
}
}
\section{IX. should ... use a declarative proof style?}
\def\sectionframeextra{}

\begin{frame}
\frametitle{proof styles in proof assistants}
\begin{itemize}
\item
\textbf{tactic scripts} \gray{\small (HOL, Isabelle, Coq, PVS, B method, Metamath)}

\red{procedural} \\
\uncover<4->{\green{only understandable by interactively replaying the proof}}

\item
\textbf{controlled natural language} \gray{\small (Mizar, Isabelle/Isar\only<6->{\lightgray}{, Twelf)}}

\red{declarative} \\
\uncover<5->{\green{similar in look to programming language}}

\item
\textbf{generated natural language} \gray{\small (ACL2\only<8>{, Theorema})}

\uncover<7->{\green{rather verbose: screens and screens of text}}

\item
\textbf{\only<3->{\gray}{actual natural language}} \only<3->{\gray{\small (not practically possible)}}

\uncover<2->{\green{\only<3->{\gray}{`computer should be able to parse mathematical {\LaTeX}'}}}

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Mohan Ganesalingam and the language of mathematics}
Mohan Ganesalingam, \pgfimage[width=10pt]{pics/flags/uk}\ University of Cambridge \\
\textsl{senior wrangler} of his year

\blue{The Language of Mathematics}, 2009 \\
277 page master's thesis $\to$ PhD thesis
\medskip

\red{articficial} language as close as possible to 
\red{actual} language
\pause
\medskip

\pgfimage[width=10pt]{pics/flags/poland}\ Andrzej Trybulec, \textbf{Mizar} \\
\pgfimage[width=10pt]{pics/flags/germany}\hspace{1.04pt}\pgfimage[width=10pt]{pics/flags/france}\ Makarius Wenzel, Isabelle/\textbf{Isar} \\
\pgfimage[width=10pt]{pics/flags/ukraine}\hspace{1.04pt}\pgfimage[width=10pt]{pics/flags/france}\ Andriy Paskevych, SAD/\textbf{ForTheL} \pause {\small (= `Evidence Algorithm')} \\\medskip\pause
\pgfimage[width=10pt]{pics/flags/usa}\ Steven Kieffer, \blue{\small A language for mathematical knowledge management}\toolong \\
\pgfimage[width=10pt]{pics/flags/germany}\ Peter Koepke, \blue{\small Naturalness in formal mathematics} \\
\pgfimage[width=10pt]{pics/flags/germany}\ Claus Zinn, \blue{\small Understanding Informal Mathematical Discourse} \\
\pgfimage[width=10pt]{pics/flags/sweden}\ Aarne Ranta, \blue{\small Syntactic categories in the language of mathematics}\toolong
\end{frame}

\begin{frame}
\def\linktitle{formal proof sketches}
\frametitle{{\only<22>{\textbf}{formal}} proof {\only<21>{\textbf}{sketches}}}
\vbox to 0pt{
\vspace{-.9em}
\uncover<1,20-21>{\begin{flushleft}
\leftskip=1.25em\rightskip=1.25em
\looseness=-1
\textbf{Theorem 43 \green{\small (Pythagoras' theorem)}.} \textsl{$\sqrt{2}$ is irrational.}\\\medskip
The traditional proof ascribed to Pythagoras runs
as follows.  If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{\textsf{(4.3.1)\hspace{\rightskip}}}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$.  Hence $a^2$ is even, and \red{there%-
fore $a$ is even.}  If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$.
\hfill$\Box$%
\end{flushleft}}
\vss
}\vspace{-1.02em}
\vbox to 0pt{
\vspace{-.9em}
\vspace{-.7em}
\uncover<2->{\begin{flushleft}
\leftskip=1.25em\small
\uncover<-3>{\textbf{theorem}} \uncover<-2>{\green{:: \textsl{Pythagoras' theorem}}} \\
\uncover<-3>{\quad Th43: sqrt 2 is irrational} \\
\uncover<-4>{\textbf{proof}} \\
\uncover<-4>{:: \textsl{the traditional proof ascribed to Pythagoras\,}:} \\
\uncover<-5>{\quad \textbf{assume} sqrt 2 is rational;} \\
\uncover<-6>{\quad \textbf{consider} a, b \textbf{such} \textbf{that}} \\
\uncover<-7>{4\_3\_1:} \uncover<-8>{a{\char`\^}2 = 2$\,*\,$b{\char`\^}2} \uncover<-9>{\textbf{and}} \\
\uncover<-10>{\qquad a,b are\_relative\_prime;} \\
\uncover<-11>{\quad \textbf{then} a{\char`\^}2 is even;} \\
\uncover<-12>{\quad \red{\textbf{then} a is even;}} \\
\uncover<-13>{\quad \textbf{consider} c \textbf{such} \textbf{that} a = 2$\,*\,$c;} \\
\uncover<-14>{\quad \textbf{then} 4$\,*\,$c{\char`\^}2 = 2$\,*\,$b{\char`\^}2;} \\
\uncover<-15>{\quad 2$\,*\,$c{\char`\^}2 = b{\char`\^}2;} \\
\uncover<-16>{\quad b is even;} \\
\uncover<-17>{\quad \textbf{hence} contradiction;} \\
\uncover<-18>{\textbf{end};}
\end{flushleft}}
\vss
}\vspace{-1.25em}
\vbox to 0pt{
\vspace{-.9em}
\uncover<-19,22>{\begin{flushleft}
\leftskip=1.25em\rightskip=1.25em
\uncover<4->{\textbf{theorem}} \uncover<4->{{\small Th\hspace{.8pt}\textbf{43}:} \textsl{sqrt 2 is irrational}} \uncover<3->{\green{\small :: \textbf{(Pythagoras' theorem)\toolong}}}\\\medskip
\uncover<5->{\textbf{proof}}\hspace{1em}\uncover<5->{:: the traditional proof ascribed to Pythagoras\,:}\hfill\break
\uncover<6->{assume sqrt 2 is rational;} \uncover<7->{consider $a, b$ such that}
$$\uncover<9->{\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}}\leqno{\mbox{\hspace{\leftskip}\uncover<8->{4\_3\_1\,:}}}$$%
\uncover<10->{and} \uncover<11->{$a,b$ are\_relative\_prime;} \uncover<12->{then $a\mathbin{\hat{}}2$ is even;}
\uncover<13->{\red{then $a$ is even;}} \uncover<14->{consider $c$ such that $a = 2\mathbin{*}c$;} \uncover<15->{then $4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$;}\break\uncover<16->{$2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$;} \uncover<17->{$b$ is
even;} \uncover<18->{hence contradiction;} \hfill \uncover<19->{end;}
\end{flushleft}}
\vss
}

\end{frame}

\begin{frame}
\frametitle{integrating the procedural and declarative proof styles}
Freek Wiedijk, \pgfimage[width=10pt]{pics/flags/netherlands}\ Radboud University Nijmegen, 2009

\red{Mizar Light = \\
Mizar proof language on top of HOL Light system}
\pause
\bigskip

three ways to create Mizar Light texts
\begin{itemize}
\item
\textbf{editing} manually \blue{= declarative proof style}

\uncover<3->{\green{check-fix-extend cycle}}

\item
\textbf{growing} by executing tactics \blue{= procedural proof style}

\uncover<4->{\green{lines without correct justification are the subgoals}}

\item
\uncover<5>{\textbf{converting} existing HOL Light scripts}

\end{itemize}

\end{frame}

\def\sectiontitle{how should the next generation of proof assistants\break be arrived at?}
\section{X. how should ... be arrived at?}

\begin{frame}
\frametitle{evolution versus revolution}
\begin{itemize}
\item
{next generation \textbf{of an existing system?}}

\uncover<2->{{\blue{{HOL Light} $\to$ Mizar Light} was an attempt at this}}
\bigskip

\uncover<3->{best starting points = \green{systems that answered {`yes'} most}

\begin{flushleft}
\setlength{\unitlength}{.92pt}
\begin{picture}(68,22)(-28,55)
\put(-28,75){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/uk}}}
\put(-16,75){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/germany}}}
\put(0,75){\makebox(0,0)[l]{\strut {\textbf{Isabelle}}}}
\put(-16,60){\makebox(0,0)[l]{\strut \pgfimage[width=10pt]{pics/flags/france}}}
\put(0,60){\makebox(0,0)[l]{\strut {\textbf{Coq}}}}
\end{picture}
\medskip
\end{flushleft}}

\item
new system \textbf{from scratch?}

\uncover<4->{\blue{throw away all that existing work?}}

\medskip
\end{itemize}

\uncover<5->{\only<6>{\gray}{many interoperable systems, or} \only<6>{\red}{let the best system win}\only<5>{?}\only<6>{\hspace{.5pt}\red{!}}}

\end{frame}

\let\sectiontitle=\nosectiontitle
\setcounter{section}{-3}

\section{the three bottlenecks}

\begin{frame}
\frametitle{main improvements needed for wide adaptation of proof assistants}
\begin{itemize}
\item
better \textbf{automation}

\item
better mathematical \textbf{libraries}

\item
better match with existing mathematical \textbf{culture}
\pause

\item
better \textbf{visual} reasoning
\pause
\smallskip

\begin{flushleft}
\leftskip=2em\rightskip=2em
\small
\blue{\textbf{theorem}\, {\normalsize $\displaystyle \only<7>{\red}{\arctan \frac{1}{2}} + \only<8>{\red}{\arctan \frac{1}{3}} = \only<9>{\red}{\frac{\pi}{4}}$} \\
\textbf{proof}}
\medskip
\pause
\uncover<5,10>{
\vspace{4.75em}

\hfill$\blue{\Box}$
\vspace{-6.25em}

}
\only<4-5>{\begingroup
\vspace{.3em}
\small
\texttt{> \green{simplify(arctan(1/2) + arctan(1/3) - Pi/4);}}
$$\pause\red{0}$$
\endgroup}
\only<6->{\vspace{-1em}%
\strut\phantom{\textbf{theorem}\, }\only<6>{\pgfimage[width=10em]{pics/proof0}}\only<7>{\pgfimage[width=10em]{pics/proof1}}\only<8>{\pgfimage[width=10em]{pics/proof2}}\only<9>{\pgfimage[width=10em]{pics/proof3}}\only<10>{\pgfimage[width=10em]{pics/proof4}}}
\end{flushleft}

\end{itemize}

\end{frame}

\end{document}