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

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

\def\headphoto#1{\vbox to 0pt{
\vspace{-0.9em}
\hfill\includegraphics[width=6.5em]{/home/freek/talks/groningen/pics/people/#1.eps}\par
\vss}\vspace{-1.4em}}

\def\xheadphoto#1#2{\vbox to 0pt{
\vspace{-0.9em}
\hfill\includegraphics[width=6.5em]{/home/freek/talks/groningen/pics/people/#1.eps}\par
\hfill\includegraphics[width=6.5em]{/home/freek/talks/groningen/pics/people/#2.eps}\par
\vss}\vspace{-1.4em}}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut formal proof with the computer}

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

\green{University of Groningen} \\
{2010\hspace{3pt}03\hspace{3pt}17, 16\hspace{1pt}:\hspace{1.8pt}15}

\end{slide}

\begin{slide}
\sectiontitle{a very brief history of formal proof}
\slidetitle{calculus ratiocinator}
\headphoto{leibniz}

Gottfried Leibniz, 1646--1716 \\
{replace reasoning with calculation\adviwait:}
\textbf{Calculemus\exclspace!}\adviwait
\bigskip

\vbox to 0pt{
\includegraphics[width=18em]{/home/freek/talks/groningen/pics/other/leibniz.eps}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{principia mathematica}
\xheadphoto{whitehead}{russell}

Alfred North Whitehead \& Bertrand Russell
\medskip

\red{{logicism}} $=$ \\
`mathematics can be seen as part of logic'
\adviwait
\bigskip
\medskip

\textbf{Principia Mathematica},
1910--1913 \\
\green{`arithmetic on the real numbers'}
\medskip
\adviwait
\adviembed{xvieww /home/freek/talks/groningen/pics/large/principia.jpg}\adviwait[1]%

`$1 + 1 = 2$' only proved on page 360

\vfill
\end{slide}

\begin{slide}
\slidetitle{Automath
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/netherlands.eps}}}
\headphoto{debruijn}

N.G. de Bruijn, 1968:
\medskip

\red{proof assistant} \\ \adviwait
\green{$=$ \advirecord{b1}{interactive}\adviplay{b1} theorem prover \\ \adviwait
%\adviplay[slidered]{b1}\adviwait
$=$ proof checker \adviwait}
\vspace{2.7em}

\headphoto{jutting}
\vspace{-0.7em}
Bert Jutting, 1979: \\
translation of \textbf{Grundlagen} by Edmund Landau
\smallskip

143 pages in German \\
\green{`arithmetic on the real numbers'}
\adviwait
\adviembed{xvieww /home/freek/talks/groningen/pics/large/automath.jpg}%
\medskip
\adviwait

full night of computer time \adviwait in 1979 \\
less than half a second in 2010

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

\begin{slide}
\sectiontitle{what formal proof looks like}
\slidetitle{between mathematics and computer science}

\begin{center}
\vspace{2em}
\begin{tabular}{c}
mathematical journal article or \green{textbook} \\
\noalign{\vspace{-\smallskipamount}}
(mathematical vernacular) \\
\gray{\advirecord{c3}{$\updownarrow$}\advirecord{c1}{\rlap{$\,^?$}}}\adviplay{c1}\adviplay{c3} \\
\red{formalization} \\
\white{\advirecord{c4}{$\updownarrow$}\advirecord{c2}{\rlap{$\,^?$}}}\red{\advirecord{c5}{\llap{$\parallel$}}}\adviplay{c4}\adviplay{c2} \\
source code of a \green{computer program}
\end{tabular}
\end{center}
\adviwait
\adviplay[white]{c1}
\adviplay[white]{c2}
\adviplay[slidelightgray]{c3}
\adviplay[white]{c4}
\adviplay[slidered]{c5}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first example:} a poem by Marjolein Kool}
\vbox to 0pt{
\vspace{-1.4em}
\def\mizar#1{\strut\rlap{\hspace{160pt}\texttt{\strut #1}}}
\begin{flushleft}\footnotesize
\offinterlineskip
\mizar{}%
\advirecord{c1}{Een bolleboos riep laatst met zwier} \\
\advirecord{c2}{\mizar{theorem}}%
\advirecord{c3}{gewapend met een vel A-vijf:} \\
\red{\advirecord{c4}{\mizar{\ \ not ex n st for m holds n >= m}}}%
\advirecord{c5}{Er is geen allergrootst getal,} \\
\advirecord{c6}{\mizar{proof}}%
\advirecord{c7}{dat is wat ik bewijzen ga.} \\
\mizar{}%
\advirecord{c8}{Stel, dat ik u nu zou bedriegen} \\
\green{\advirecord{c9}{\mizar{\ \ assume not thesis;}}}%
\advirecord{c10}{en hier een potje stond te jokken,} \\
\green{\advirecord{c11}{\mizar{\ \ then consider n such that}}}%
\advirecord{c12}{dan ik zou zonder overdrijven} \\
\white{\advirecord{cx1}{\mizar{\ \ let n;}}}%
\green{\advirecord{c13}{\mizar{\rlap{\advirecord{c37}{A1:}}\ \ \ \ for m holds n \char`\>= m;}}}%
\advirecord{c14}{het grootste kunnen op gaan noemen.} \\
\mizar{}%
\advirecord{c15}{Maar ben ik klaar, roept u gemeen:} \\
\green{\advirecord{c16}{\mizar{\ \ set n' = n + 2;}}}%
\advirecord{c17}{`Vermeerder dat getal met twee!'} \\
\mizar{}%
\advirecord{c18}{En zien we zeker en gewis} \\
\white{\advirecord{cx2}{\mizar{\ \ n + 2 > n by XREAL\char`\_1:31;}}}%
\green{\advirecord{c19}{\mizar{\ \ n' > n\rlap{\white{\advirecord{c35}{;}}}\ \advirecord{c38}{by XREAL\char`\_1:31;}}}}%
\advirecord{c20}{dat dit toch niet het grootste was.} \\
{\mizar{\ \ \ \ \ \ \ \white{\advirecord{c33}{*4}}}}%
\advirecord{c22}{En gaan we zo nog door een poos,} \\
\green{\advirecord{c23}{\mizar{\ \ then not for m holds n >= m;}}}%
\advirecord{c24}{dan merkt u: dit is onbegrensd.} \\
\mizar{}%
\advirecord{c25}{En daarmee heb ik q.e.d.} \\
\white{\advirecord{cx3}{\mizar{\ \ hence thesis;}}}%
\green{\advirecord{c26}{\mizar{\ \ hence contradiction\rlap{\white{\advirecord{c36}{;}}}\ \advirecord{c39}{by A1;}}}}%
\advirecord{c27}{Ik ben hier diep gelukkig door.} \\
{\mizar{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \white{\advirecord{c34}{*1}}}}%
\advirecord{c29}{`Zo gaan', zei hij voor hij bezwijmde,} \\
\advirecord{c30}{\mizar{end;}}%
\advirecord{c31}{`bewijzen uit het ongedichte'.}
\end{flushleft}
\vss
\adviplay{c1}
\adviplay{c3}
\adviplay{c5}
\adviplay{c7}
\adviplay{c8}
\adviplay{c10}
\adviplay{c12}
\adviplay{c14}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c22}
\adviplay{c24}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviwait
\adviplay[slideblue]{x1}
\adviplay[slideblue]{x2}
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay[slidegreen]{c1}
\adviplay[slidegreen]{c2}
\adviplay[slidegreen]{c3}
\adviwait
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay[slidegreen]{c4}
\adviplay[slidegreen]{c5}
\adviwait
\adviplay{c4}
\adviplay{c5}
\adviplay[slidegreen]{c6}
\adviplay[slidegreen]{c7}
\adviwait
\adviplay{c6}
\adviplay{c7}
\adviplay[slidegreen]{c8}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c10}
\adviwait
\adviplay{c8}
\adviplay{c9}
\adviplay{c10}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c12}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c14}
\adviwait
\adviplay{c11}
\adviplay{c12}
\adviplay{c13}
\adviplay{c14}
\adviplay[slidegreen]{c15}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c17}
\adviwait
\adviplay{c15}
\adviplay{c16}
\adviplay{c17}
\adviplay[slidegreen]{c18}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c20}
\adviplay[slidegreen]{c35}
\adviwait
\adviplay{c18}
\adviplay{c19}
\adviplay{c20}
\adviplay{c35}
\adviplay[slidegreen]{c22}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c24}
\adviwait
\adviplay{c22}
\adviplay{c23}
\adviplay{c24}
\adviplay[slidegreen]{c25}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c27}
\adviplay[slidegreen]{c36}
\adviwait
\adviplay{c25}
\adviplay{c26}
\adviplay{c27}
\adviplay{c36}
\adviplay[slidegreen]{c29}
\adviplay[slidegreen]{c30}
\adviplay[slidegreen]{c31}
\adviwait
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay{c30}
\adviplay[slidered]{c33}
\adviplay[slidered]{c34}
\adviwait
\adviplay[white]{c34}
\adviplay[white]{c36}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c33}
\adviplay[white]{c35}
\adviplay[slidegreen]{c38}
\adviwait
\adviplay{c37}
\adviplay{c38}
\adviplay{c39}
\adviplay[slidered]{c4}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c38}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c9}
\adviplay[white]{c11}
\adviplay[white]{c13}
\adviplay[white]{c37}
\adviplay[white]{c16}
\adviplay[white]{c19}
\adviplay[white]{c38}
\adviplay[white]{c23}
\adviplay[white]{c26}
\adviplay[white]{c39}
\adviplay[slidegreen]{cx1}
\adviplay[slidegreen]{cx2}
\adviplay[slidegreen]{cx3}
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{second example:} an {\small IMO} puzzle}

\textbf{Problem.}
{%
%Let $f$ and $g$ be real-valued functions.
\green{For all $x$ and $y$ $$f(x + y) + f(x - y) = 2 f(x) g(y)$$}%
\green{$|f(x)| \le 1$ for all $x$}, and $f$ is not identically zero. \\
\red{Prove that $|g(x)| \le 1$ for all $x$.}
}
\adviwait

{\small
\bigskip
\textbf{Solution.}
Let $k$ be the least upper bound for $|f(x)|$. \adviwait \\
Suppose $|g(y)| > 1$ for some $y$. \adviwait
Then
$$2k \ge |f(x + y)| + |f(x - y)| \ge |f(x + y) + f(x - y)| = 2 |f(x)||g(y)|\adviwait$$
This implies that $|f(x)| \le k/|g(y)|$. \adviwait \\
In other words $k/|g(y)|$ is an upper bound for $|f(x)|$. \adviwait \\
But this is less than $k$.
Contradiction.\hfill$\Box$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} in {\small HOL} Light
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/uk.eps}$\,$%
\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/usa.eps}}}
\vbox to 0pt{
\vspace{-1.0em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
let IMO = prove
 (`\red{!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\\
         ~(!x. f(x) = &0) /\\
         (!x. abs(f(x)) <= &1)
         ==> !x. abs(g(x)) <= &1}`,
  \green{let LL = REAL_ARITH `&1 < k ==> &0 < k` in
  REPEAT STRIP_TAC THEN SPEC_TAC(`x:real`,`y:real`) THEN
  ABBREV_TAC `k = sup (IMAGE (\\x. abs(f(x))) (:real))` THEN
  MP_TAC(SPEC `IMAGE (\\x. abs(f(x))) (:real)` SUP) THEN
  ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV] THEN
  ANTS_TAC THENL [ASM SET_TAC[]; STRIP_TAC] THEN
  SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `k / abs(g(y:real))`) THEN
  SIMP_TAC[NOT_IMP; NOT_FORALL_THM] THEN CONJ_TAC THENL
   [ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL;
      REAL_ARITH `u + v = &2 * z /\\ abs u <= k /\\ abs v <= k ==> abs z <= k`];\toolong
    ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL; REAL_MUL_RID; LL;\toolong
      REAL_ARITH `~(z = &0) /\\ abs z <= k ==> &0 < k`]]});;
\end{alltt}
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} in Coq
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/france.eps}}}
\vbox to 0pt{
\vspace{-1.0em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
Theorem imo1972:
 \red{forall f g: R -> R,
 (forall x y: R,  f (x + y) + f (x - y) = 2 * f x * g y) ->
 ~ (forall x: R, f x = 0) ->
 Rfbound f 1 -> Rfbound g 1}.
\green{intros f g Eq Nz Rf1 y.
case (Rle_or_lt (Rabs (g y)) 1); intros H; auto.
case (Rflub_def f _ Rf1); clear Rf1.
intros k [Kb Kl].
assert (Kp: 0 < k); [idtac | clear Nz].
 case (Rle_or_lt k 0); auto; intros H1.
 case Nz; intros x.
 assert (HH: forall x, Rabs x = 0 -> x = 0);
  [intros x1; ffourier | idtac].
 apply HH; clear HH.
 apply Rle_antisym; [idtac | apply Rabs_pos].
 assert (HH := Kb x); ffourier.}\smallskip
\blue{\textsf{\normalsize\textsl{etcetera}}}
\end{alltt}
\endgroup
\vss
}
\adviwait
\adviembed{emacs /home/freek/talks/groningen/demo.v}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} in Mizar
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/poland.eps}}}
\vbox to 0pt{
\vspace{-1.0em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
theorem
  \red{(for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y) &
  (ex x st f.x<>0) & (for x holds abs(f.x)<=1)
  implies for x holds abs(g.x)<=1}
  proof
    \green{assume that
A1: for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y;
    given z such that
A2: f.z<>0;
    assume
A3: for x being Element of REAL holds abs(f.x)<=1;
    let y such that
A4: abs(g.y) > 1;
    set X = rng abs f, k = upper_bound X, D = abs(g.y);
A5: abs(g.y) > 0 by A4,XREAL_1:2;
A6: X is bounded_above
    proof}\smallskip
\blue{\textsf{\normalsize\textsl{etcetera}}}
\end{alltt}
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} and in Isabelle
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/uk.eps}$\,$%
\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/germany.eps}}}
\vbox to 0pt{
\vspace{-1.0em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
theorem IMO:
   \red{assumes "ALL (x::real) y. f(x + y) + f(x - y) = (2::real) * f x * g y"\toolong
   and "~ (ALL x. f(x) = 0)"
   and "ALL x. abs(f x) <= 1"
   shows "ALL y. abs(g y) <= 1"}
proof \green{(clarify, rule leI, clarify)
   obtain k where "isLub UNIV {z. EX x. abs(f x) = z} k"
     by (subgoal_tac "EX k. ?P k", force, insert prems,
         auto intro!: reals_complete isUbI setleI)
   hence "ALL x. abs(f x) <= k"
     by (intro allI, rule isLubD2, auto)
   fix y
   assume "abs(g y) > 1"
   have "ALL x. abs(f x) <= k / abs(g y)"
   proof
     fix x
     have "2 * abs(g y) * abs(f x) = abs(f(x + y) + f(x - y))"}\smallskip
\blue{\textsf{\normalsize\textsl{etcetera}}}
\end{alltt}
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof versus artificial intelligence}
\adviwait\headphoto{robbins0}
\vspace{-2em}

$$
\begin{array}{c}
a \lor b = b \lor a \\
a \lor (b \lor c) = (a \lor b) \lor c \\
\red{\neg(\neg(a \lor b) \lor \neg (a \lor \neg b)) = a}
\end{array}
\hspace{8em}
$$

\vspace{1em}
Herbert Robbins, 1933: \green{always a Boolean algebra?}
\adviwait
\vspace{0.1em}
\smallskip

\headphoto{mccune}
\vspace{.4em}
William McCune + {\small EQP}, 1996: \green{34 line proof}

eight days of computer time

\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof versus computer algebra}

\texttt{\small > \green{\advirecord{d1}{2*infinity-infinity}\white{\advirecord{d2}{\rlap{;}}}\advirecord{d3a}{,}\advirecord{d3}{ 2*x-x;}}}\adviplay[slidered]{d1}\adviplay[slidered]{d2}\adviwait
{\vspace{-\smallskipamount}}
$$\white{\advirecord{d4}{\rlap{\hspace{6pt}undefined}}}\advirecord{d5a}{{\sf undefined}\hspace{.5pt},\,}\advirecord{d5}{x}\adviplay{d4}\adviwait\adviplay[slidegray]{d1}\adviplay[white]{d2}\adviplay[white]{d4}\adviplay[slidegray]{d3a}\adviplay[slidegreen]{d3}\adviplay{d5}\adviplay[slidegray]{d5a}\adviwait\adviplay[slidegreen]{d1}\adviplay[slidegreen]{d3a}\adviplay[black]{d5a}$$

\texttt{\small > \green{subs(x=infinity, 2*x-x);}}
{\vspace{-\smallskipamount}}
$${\sf infinity}\adviwait\bigskip$$

\texttt{\small > \white{\rlap{\advirecord{d6a}{1/(1-x) = }\advirecord{d6b}{simplify(}\advirecord{d6c}{1/(1-x)}\advirecord{d6d}{)}\advirecord{d6e}{;}}}\adviplay[slidegreen]{d6a}\adviplay[slidered]{d6b}\adviplay[slidegreen]{d6c}\adviplay[slidered]{d6d}\adviplay[slidegreen]{d6e}%
\green{\advirecord{d7a}{int(}\advirecord{d7b}{1/(1-x)}\advirecord{d7c}{,x)}\advirecord{d7d}{ = }\advirecord{d7e}{int(}\advirecord{d7f}{simplify(1/(1-x))}\advirecord{d7g}{,x)}\advirecord{d7h}{;}}}
{\vspace{-\smallskipamount}}
$$\white{\advirecord{d8}{{1 \over 1 - x} = -{1 \over -1 + x}}}\adviplay{d8}\adviwait$$
\adviplay[white]{d6a}\adviplay[white]{d6b}\adviplay[white]{d6c}\adviplay[white]{d6d}\adviplay[white]{d6e}
\adviplay[slidered]{d7a}
\adviplay[slidegreen]{d7b}
\adviplay[slidered]{d7c}
\adviplay[slidegreen]{d7d}
\adviplay[slidered]{d7e}
\adviplay[slidegreen]{d7f}
\adviplay[slidered]{d7g}
\adviplay[slidegreen]{d7h}
\adviplay[white]{d8}%
{\vspace{-3.75em}}
$$-\ln(1 - x) = -\ln(-1 + x)\adviwait
\adviplay[slidegreen]{d7a}
\adviplay[slidegreen]{d7c}
\adviplay[slidegreen]{d7e}
\adviplay[slidegreen]{d7g}
$$

\texttt{\small > \green{evalf(subs(x=-1, \char`\%));}}
{\vspace{-\smallskipamount}}
$$-0.6931471806 = -0.6931471806 - 3.141592654 i$$

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

\begin{slide}
\slidetitle{the de Bruijn criterion}
all software has bugs$\,$\dots \\
\red{why trust a proof checker?}
\medskip
\adviwait

%{{N.G.~de Bruijn}, 1968}:
\begin{quote}
{{\small [$\,$\dots]$\,$}
\green{This is one of the reasons for keeping {\small AUTOMATH} as primitive
as possible.}
\small{[$\,$\dots]}}
\end{quote}
\bigskip
\smallskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\red{{small independent checker(s)}} \\
{Ivy system} for Otter/Prover9

\medskip
\adviwait
\item[$\bullet$]

\red{{small proof checking \textbf{kernel} inside the system}} \\
\blue{{{\small LCF} architecture}}
\smallskip

{{Robin Milner}, 1972}
\vspace{-7em}

\headphoto{milner1}

\end{itemize}

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

\begin{slide}
\sectiontitle{state of the art in formal proof}
\slidetitle{the {\small ARM} microprocessor}
\begin{center}
\vbox to 0pt{
\vspace{-1.6\medskipamount}
\includegraphics[height=18em]{/home/freek/talks/groningen/pics/other/arm0.eps}
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} proved correct in {\small HOL}4 by Anthony Fox}
{University of Cambridge, 2002}

\begin{center}
\bigskip
\vbox to 0pt{
\vspace{-1.6\medskipamount}
\begingroup
\setlength\tabcolsep{0pt}
\begin{tabular}{cc}
\includegraphics[width=15em]{/home/freek/talks/groningen/pics/other/arm1.eps} &
\includegraphics[width=15em]{/home/freek/talks/groningen/pics/other/arm2.eps} \\
\noalign{\bigskip}
{\small ARM}6 architecture & {\small ARM}v3 instruction set
\end{tabular}
\endgroup
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{an optimizing compiler}
\begin{center}
\vspace{-\medskipamount}
\vbox to 0pt{
\vspace{-1.6\medskipamount}
\includegraphics[width=28em]{/home/freek/talks/groningen/pics/other/compcert.eps}
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} proved correct in Coq by Xavier Leroy}
\headphoto{xavier}
{{\small INRIA}, France, 2006}
\bigskip

{optimizing compiler} \\
{\dots} \textsl{programmed} in \blue{Coq}'s functional language \\
%{\dots} executed by the Coq virtual machine \\
{\dots} compiling \textsl{from} \blue{C} \\
{\dots} compiling \textsl{to} \blue{machine code}
\adviwait
\bigskip

\begin{alltt}\small
Theorem \red{transf_c_program_correct}:
  \green{forall p tp beh,
  transf_c_program p = OK tp ->
  not_wrong beh ->
  Csem.exec_program p beh ->
  Asm.exec_program tp beh}.
\end{alltt}

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

\begin{slide}
\slidetitle{the L4 operating system}

{microkernel} \\
$\approx$ hypervisor
\bigskip

\textbf{seL4} \\
\green{implementation of L4 kernel} \\
programmed in C
\adviwait
\bigskip

\red{8,700 lines of C} + 600 lines of {\small ARM} assembly \\
2 person-years for the implementation
\adviwait
\smallskip

200,000 lines of Isabelle \\
\red{20 person-years} for the correctness proof
\smallskip

160 bugs before verification \\
\red{0 bugs} after verification \adviwait \blue{(?)}

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

\begin{slide}
\slidetitle{{\dots} proved correct in Isabelle by Gerwin Klein}
\headphoto{gerwin}
{{\small NICTA}, Australia, 2009}
\bigskip

\vbox to 0pt{
\vspace{-1.6\medskipamount}
\includegraphics[width=21em]{/home/freek/talks/groningen/pics/other/l4.eps}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the prime number theorem}
Jacques Hadamard, Charles Jean de la Vall\'ee-Poussin, 1896
$$\red{\lim_{n\to\infty} {\pi(n) \over ({n\over\ln n})} = 1}\bigskip$$

\green{number of primes $\le$ given number}
\begin{eqnarray*}
\green{\pi(1000000000000)} &=& 37607912018 \\
\noalign{\smallskip}
\adviwait
{1000000000000\over\ln(1000000000000)} &=& 36191206825.27\ldots \\
\noalign{\smallskip}
\adviwait
\int_2^{1000000000000} \!{dx\over\ln(x)} &=& 37607950279.75\ldots
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\adviembed{xvieww /home/freek/talks/groningen/pics/large/newman1.jpg}\adviwait[1]%
\slidetitle{{\dots} proved correct in {\small HOL} Light by John Harrison}
\headphoto{johnh}
Intel Oregon research center, 2008\adviwait
\vspace{-1em}

$$\green{2\pi i F(w) = \int_{\red{\Gamma}} F(z + w) N^z \left({1 \over z} + {z \over R^2}\right) dz}
\hspace{9em}\medskip$$
\begin{center}
\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*{3}}}
\put(15,0){\line(1,0){5}}
\put(15,40){\line(0,-1){40}}
\put(15,40){\line(1,0){5}}
\put(20,0){\advirecord{f1}{\circle*{2}}}
\put(20,40){\advirecord{f2}{\circle*{2}}}
\end{picture}}\hspace{9em}\strut
\vspace{-\medskipamount}
\end{center}
\adviwait

\vbox to 0pt{
\vspace{-.5em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\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{alltt}
\endgroup
\vss}
\adviplay[slidered]{f1}
\adviplay[slidered]{f2}

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

\begin{slide}
\slidetitle{the four color theorem}
\begin{center}
\vbox to 0pt{
\vspace{-1.6\medskipamount}
\includegraphics[height=18em]{/home/freek/talks/groningen/pics/other/4ct.eps}
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} proved correct in Coq by Georges Gonthier}
\headphoto{georges1}
\vbox to 0pt{
\vspace{-1.0em}
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\footnotesize
Lemma unavoidability : \red{reducibility ->
  forall g, ~ minimal_counter_example g}.
Proof.
\green{move=> Hred g Hg; case: (posz_dscore Hg) => x Hx.
have Hgx: valid_hub x by split.
have := (Hg : pentagonal g) x;
  rewrite 7!leq_eqVlt leqNgt.
rewrite exclude5 ?exclude6 ?exclude7 ?exclude8
  ?exclude9 ?exclude10 ?exclude11 //.
case/idP; apply: (@dscore_cap1 g 5) => \{x n Hn Hx Hgx\}// y.
pose x := inv_face2 y; pose n := arity x.
have ->: y = face (face x) by rewrite /x /inv_face2 !Enode.
rewrite (dbound1_eq (DruleFork (DruleForkValues n))) // leqz_nat.\toolong
case Hn: (negb (Pr58 n)); first by rewrite source_drules_range //.\toolong
have Hrp := no_fit_the_redpart Hred Hg.
apply: (check_dbound1P (Hrp the_quiz_tree) _
  (exact_fitp_pcons_ Hg x)) => //.
rewrite -/n; move: n Hn; do 9 case=> //.}
Qed.
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Feit-Thompson project of Georges Gonthier
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/usa.eps}$\,$%
\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/france.eps}}}

\begin{center}
\bigskip
\includegraphics[width=16em]{/home/freek/talks/groningen/pics/other/joint.eps}
\end{center}
\adviwait
\bigskip
\bigskip

\textbf{Feit-Thompson} theorem \\
\red{every finite group of odd order is solvable}
\bigskip
\medskip
\adviwait

\green{`{It takes a professional group theorist about a year of hard work to}
\white{\advirecord{i1}{\rlap{understand}}}\advirecord{i2}{\textsl{understand}}\adviplay{i1} {the proof completely.}'}
\vspace{-\bigskipamount}

\strut\hfill---$\;$Wikipedia\quad\strut
\adviwait\adviplay[white]{i1}\adviplay[slidegreen]{i2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Flyspeck project of Tom Hales
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/usa.eps}$\,$%
\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/vietnam.eps}}}
\headphoto{hales}
\vspace{-2.5em}

\includegraphics[width=18em]{/home/freek/talks/groningen/pics/other/flyspeck.eps}
\vspace{-.5em}

\textbf{Kepler conjecture}, 1661:
is this the \red{densest sphere packing} possible? \\
Tom Hales, 1998: yes\exclspace!
\adviwait
\medskip

3 gigabytes of data,
couple of months of computer time \\
referees \green{99\% certain} that everything is correct

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

\begin{slide}
\sectiontitle{why current systems for formal proof are not perfect yet}
\slidetitle{all of the undergraduate curriculum?}

\textbf{de Bruijn factor} \\
= \green{ratio in size between \white{\advirecord{h2}{\rlap{formal and textbook mathematics}}}\advirecord{h1}{(gzipped) formal and textbook mathematics}\adviplay{h2}}\adviwait
$$\red{\approx 4}\adviwait\adviplay[white]{h2}\adviplay[slidegreen]{h1}\adviwait$$
\green{de Bruijn factor in time}
$$ \approx {\textstyle 2{1\over 2}}\,{\mbox{person-year}\over{\sf megabyte}}\red{\,{}\approx 1\, {{\sf week}\over{\sf textbook\ page}}}\adviwait\bigskip$$

\green{formalizing \textsl{all} basic mathematics}:
the \textbf{Drake equation}
$$12\cdot 400\cdot 3\cdot 4\cdot {2{1\over 2}\over 1024} \red{{}\approx 140 \;\mbox{person-years}}\adviwait
\,\approx 15\cdot 10^6\;\mbox{\euro} \,\approx 1\;{\sf Hollywood\ movie}$$

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

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

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\red{
\begin{picture}(5,5)
\put(0.5,4.5){\makebox(0,0){\white{\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}}
\put(1.5,4.5){\makebox(0,0){\white{\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}}
\put(2.5,4.5){\makebox(0,0){\white{\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}}
\put(3.5,4.5){\makebox(0,0){\white{\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}}
\put(3.5,3.5){\makebox(0,0){\white{\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}}
\put(2.5,3.5){\makebox(0,0){\white{\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}}
\put(1.5,3.5){\makebox(0,0){\white{\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}}
\put(0.5,3.5){\makebox(0,0){\white{\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}}
\put(0.5,2.5){\makebox(0,0){\white{\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}}
\put(0.5,1.5){\makebox(0,0){\white{\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}}
\put(0.5,0.5){\makebox(0,0){\white{\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}}
\put(1.5,0.5){\makebox(0,0){\white{\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}}
\put(1.5,1.5){\makebox(0,0){\white{\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}}
\put(2.5,1.5){\makebox(0,0){\white{\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}}
\put(2.5,0.5){\makebox(0,0){\white{\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}}
\put(3.5,0.5){\makebox(0,0){\white{\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}}
\put(4.5,0.5){\makebox(0,0){\white{\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}}
\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[slidered]{e0}
\end{picture}
}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slidered]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidered]{e0}%

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

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

{\small HOL}4, {\small HOL} Light, Coq, Isabelle old style, {\small PVS}, B method%, Metamath\toolong

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

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

Mizar, Isabelle new style, {\small ACL}2

\end{itemize}

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

\begin{slide}
\slidetitle{incompatible foundations}
\begin{itemize}
\item[$\bullet$]
\textbf{set theory} \\
Mizar, Isabelle/{\small ZF}, B method \\ %, Metamath \\
\green{often untyped}

\item[$\bullet$]
\textbf{higher order logic} \\
{\small HOL}4, {\small HOL Light}, Isabelle/{\small HOL}, {\small PVS} \\
\green{weak version of set theory (\red{$V_{\omega+\omega}$}),
typed}

\item[$\bullet$]
\textbf{primitive recursive arithmetic} \\
{\small ACL}2 \\
\green{\textbf{very} weak foundation (\red{no $\exists$}),
untyped,
computational}

\item[$\bullet$]
\textbf{type theory} \\
Coq \\
\green{as strong as set theory,
typed,
computational,} \blue{intuitionistic}

\end{itemize}

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

\begin{slide}
\slidetitle{intuitionism
\hfill\raise-1pt\hbox{\includegraphics[width=16pt]{/home/freek/talks/groningen/pics/flags/netherlands.eps}}}
\headphoto{brouwer}

\textbf{halting problem}
\medskip

\green{$\mbox{\large$\forall$} M\in \mbox{\sf Turing machines}$ \\
$\strut\quad\big((M \mbox{\sf\ terminates}) \lor \neg (M \mbox{\sf\ terminates})\big)$}

is \red{unprovable}
\adviwait
\bigskip
\bigskip

\textbf{intermediate value theorem}
\medskip

\green{$\mbox{\large$\forall$} \blue{f : {\mathbb R} \to {\mathbb R}}$ \\
$\strut\quad \big(f(0) < 0 \land f(1) > 0 \Rightarrow \exists x \in (0,1) \; (f(x) = 0)\big)$}

is \red{unprovable}

\vbox to 0pt{
\vspace{-5.5em}
\setlength\unitlength{.108333em}
\hfill\begin{picture}(70,50)(-10,-10)
\gray{
\put(0,-5){\line(0,1){50}}
\put(60,-5){\line(0,1){50}}
\put(0,-7){\makebox(0,0)[tc]{$0$}}
\put(60,-7){\makebox(0,0)[tc]{$1$}}
}
\put(0,20){\line(1,0){60}}
\thicklines
\blue{
\put(0,0){\line(1,1){20}}
\put(20,20){\line(1,0){20}}
\put(40,20){\line(1,1){20}}
\put(31,23){\makebox(0,0)[cb]{$f$}}
}
\end{picture}\hspace{0em}\strut
\vss}


\vfill
\end{slide}

\begin{slide}
\slidetitle{undefinedness}
$$\mbox{{$\displaystyle {1 \over \red{\advirecord{e1}{0}}\adviplay{e1}} = 0$} \textbf{?}}\medskip\adviwait$$

\begin{center}
\setlength\tabcolsep{0em}
\def\lead{\gray{$\,$\leaders\hbox to .5em{\hss.\hss}\hfill}$\;$\strut}
\begin{tabular}{ll}
{\small HOL} Light$\,$\gray{\leaders\hbox to .5em{\hss.\hss}\qquad}$\;$\strut & provable \adviwait\\
{\small Coq}\lead & not provable, negation not provable \adviwait\\
{\small IMPS}\lead & negation provable \adviwait\\
{\small PVS}\lead & \green{not a correct formula}
\end{tabular}$\hspace{-6.5em}$
\end{center}
\adviwait
\medskip

$$\hspace{1em}\forall x \in {\mathbb R} \;\big(\white{\advirecord{g1}{\rlap{$\displaystyle{1\over\advirecord{g2}{x}} \ne 0\big)$ \textbf{?}}}}\adviplay[slidered]{e1}\adviplay{g1}\adviplay[slidered]{g2}\adviwait\adviplay{e1}\adviplay[white]{g1}\adviplay[white]{g2}\green{x \ne 0 \,\mathrel{\Rightarrow}\;} {1\over {x}}\ne 0\big)\mbox{ \textbf{?}}\adviwait$$
$$\hspace{1em}\forall x \in {\mathbb R} \;\big(\green{x = 0 \;\mathrel{\lor}\;\,} {1\over {x}}\ne 0\big)\mbox{ \textbf{?}}\adviwait\adviplay[slidered]{e1}$$
$$\hspace{1em}\forall x \in {\mathbb R} \;\big({1\over \red{x}} \ne 0 \,\lor\; x = 0\big)\mbox{ \textbf{?}}$$

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

\begin{slide}
\slidetitle{formal libraries}
\vspace{-1.44em}

\begin{itemize}
\item[$\bullet$]
\textsl{beautifully integrated, but \red{made by an isolated genius}}

\begin{itemize}
\item
John Harrison's {\small HOL} Light library

\item
Georges Gonthier's Ssreflect library

\end{itemize}

\item[$\bullet$]
\textsl{made by a whole community, but \red{not well integrated}}

\begin{itemize}
\item
Mizar's {\small MML}

\item
Coq's contribs

\item
Isabelle's {\small AFP}

\end{itemize}
\end{itemize}
\medskip
\smallskip
\adviwait

Nijmegen's \blue{{MathWiki project}} just started \\
1 postdoc + 1 PhD student

\green{formalizations + `Proof General on the web' + `Wikipedia for math'} \\
{Coq + Mizar + Isabelle + \dots}

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

\begin{slide}
\sectiontitle{the future of formal proof}
\slidetitle{{\small QED} manifesto}
\headphoto{boyer}
anonymous manifesto, 1994
\medskip

\begin{flushleft}
\rightskip=9.5em plus 2em
\pretolerance=10000
\green{\textsl{{\small QED} is the very tentative title of a project to build a computer
system that effectively represents all important mathematical
knowledge and techniques.} [$\,$\dots] \medskip\\
\textsl{The {\small QED} project will be a major scientific undertaking requiring the
cooperation and effort of hundreds of deep mathematical minds,
considerable ingenuity by many computer scientists, and broad support
and leadership from research agencies.}}
\end{flushleft}

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

\begin{slide}
\slidetitle{formal proof as extreme mathematics}

\begin{quote}
\medskip
\gray{\textsl{%
Coq proofs are developed interactively using a number of tactics
as elementary proof steps.
The sequence of tactics used constitutes the proof script.
\red{Building such scripts is surprisingly addictive in a
videogame kind of way}, but reading and reusing them when
specifications change is difficult.}}
\smallskip

\hfill---$\;$Xavier Leroy, \textsl{On proving in Coq}
\end{quote}
\bigskip
\bigskip
\bigskip
\adviwait

\begin{center}
\green{everyday reasoning $:$ mathematics = mathematics $:$ formal proof}
\medskip
\adviwait

\red{formal proof = mathematics$^{\sf 2}$}\adviwait\rlap{ \lightgray{$/$ informal reasoning}}
\end{center}

\vfill
\end{slide}

\end{document}