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

\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{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.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}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\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{-6em}$}

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

\def\eps{eps}

\def\webad#1#2#3{\vspace{-1.4em}\vbox to 0pt{\vspace{20em}\hspace{0em}\footnotesize\rlap{\gray{google \fbox{{\tiny\strut}\blue{\advirecord{x1}{#1}}\adviplay[slideblue]{x1}} $\,\mapsto$ {\small $\langle\hspace{.5pt}$}\texttt{http://\blue{\advirecord{x2}{#2}}\adviplay[slideblue]{x2}#3}{\small $\hspace{.5pt}\rangle$}}}\vss}}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large formalization of mathematics}

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

\red{Nederlands Mathematisch Congres} \\
Leiden University
\smallskip

2007\hspace{2pt}04\hspace{1.5pt}12, 11\hspace{.5pt}:\hspace{1pt}45
\end{slide}

\begin{slide}
\sectiontitle{what is formalization?}
\slidetitle{principia mathematica}
\begin{itemize}
\item[$\bullet$]
{Gottlob Frege}, 1879 \\
\textbf{Begriffsschrift}

\green{formal logic in theory}
\medskip

\item[$\bullet$]
{Alfred North Whitehead \& Bertrand Russell}, 1910--1913 \\
\textbf{Principia Mathematica}

\green{formal logic in practice}
\medskip

\red{development of mathematics in a formal system}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\adviembed{/home/freek/talks/nmc/bin/scans}\adviwait%
%\adviembed{xvieww /home/freek/talks/nmc/pix/principia.jpg}\adviwait[1]%
\slidetitle{automath}
\strut\hfill\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/netherlands.\eps}$\hspace{-.7pt}$\vspace{-1.19\bigskipamount}

\begin{itemize}
\item[$\bullet$]
N.G. de Bruijn, 1968 \\
\textbf{Automath}
%\adviwait
%\adviembed{xvieww /home/freek/talks/nmc/pix/automath.jpg}\adviwait[1]%

\red{computer makes formalization feasible}
\medskip
\adviwait

\item[$\bullet$]
1971--1976 \\
{large ZWO} ($\leadsto$ NWO) {project}

\item[$\bullet$]
Bert van Benthem Jutting, 1977 \\
\textbf{Checking Landau's `Grundlagen' in the Automath System}
\medskip
\smallskip

\green{158 pages of German mathematics} $\leadsto$ \\
{491 pages of Automath source code} \\
%\smallskip
%
checking time: couple of hours\enskip
\adviwait
{\small (today: under half a second)}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{what formalization isn't: \textbf{proofs with heavy computer support}}
\begin{itemize}
\item[$\bullet$]
Kenneth Appel \& Wolfgang Haken, 1977 \\
\textbf{four color theorem}

\begin{center}
\textsl{
\green{a good mathematical proof is like a poem -- \\ this is a telephone directory!}
}
\end{center}
\smallskip

\item[$\bullet$]
Andrew Odlyzko \& Herman te Riele, 1985 \\
\textbf{Mertens' conjecture}
\smallskip

first 2000 zeroes of the Riemann zeta function to 100 decimals
\medskip

\item[$\bullet$]
Tom Hales, 2003 \\
\textbf{Kepler conjecture}
\medskip

\end{itemize}

\red{computer only used as a calculator}

\vfill
\end{slide}

\begin{slide}
\slidetitle{what formalization isn't: \textbf{computer algebra}}
\vspace{-1.4em}
\vbox to 0pt{
\vspace{-1.17em}
$$\white{\advirecord{a1}{\int_0^\infty {e^{-(x-1)^2}\over\sqrt{x}} dx}}$$
\adviplay{a1}
\adviwait
\adviplay[white]{a1}
\vss
}
\hbox to 0pt{\vbox to 0pt{
\vspace{-1.17em}
\begin{alltt}
\white{\advirecord{a0x}{> int(exp(-(x-1)^2)/sqrt(x), x=0..infinity);}}\adviplay{a0x}\adviwait
\end{alltt}
$$\white{\advirecord{a0y}{\int_0^\infty {e^{-(x-1)^2}\over{x^{1\over 2}}} dx}}\adviplay[slidegreen]{a0y}$$
\adviwait
\adviplay[white]{a0x}
\adviplay[white]{a0y}
\vss
}\hss}%
\vbox to 0pt{
\vspace{-1.17em}
\begin{alltt}
> int(exp(-(x-\advirecord{a0}{t}\adviplay[slidered]{a0})^2)/sqrt(x), x=0..infinity);
\end{alltt}
$$\green{{1\over 2} {e^{-t^2} \Big({-{3 (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{3\over 4\rlap{\phantom{\tiny g}}}({t^2\over 2}) \over t^{2\rlap{\phantom{x}}}}} + {\textstyle (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{7\over 4}({t^2\over 2})} \Big) \over \pi^{1\over 2}}}\adviwait\adviplay{a0}$$
\begin{alltt}
> subs(t=1,%);
\end{alltt}
%\adviwait
$$\green{{1\over 2} {e^{-1} \big({-3 \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{3\over 4}({1\over 2})} + \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{7\over 4}({1\over 2})\big) \over \pi^{1\over 2}}}\adviwait$$
\begin{alltt}
> evalf(%);
\end{alltt}
%\adviwait
$$\green{0.4118623312}\adviwait$$
\begin{alltt}
> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));
\end{alltt}
%\adviwait
$$\green{1.973732150}\hspace{.5em}\medskip
\adviwait
$$
\red{clearly no proofs are involved here}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{what formalization isn't: \textbf{automated theorem proving}}
is every \textbf{Robbins algebra} a Boolean algebra?
$$
\green{
\begin{array}{c}
a \lor b = b \lor a \\
a \lor (b \lor c) = (a \lor b) \lor c \\
\neg(\neg(a \lor b) \lor \neg (a \lor \neg b)) = a
\end{array}
}
\smallskip
$$
\textbf{EQP} (by Bill McCune, Argonne National Laboratory), 1996: \\
\blue{`yes', with a 34 line proof}
\adviwait

\bigskip

in practice automated theorem proving is almost useless

just mindless search \\
computers only beat humans at `puzzles'
%\medskip

\red{don't expect computers to produce interesting proofs on their own}

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

\begin{slide}
\slidetitle{and now, an example: \textbf{a proof by contradiction} {\white{\advirecord{c32}{\rlap{(Marjolein Kool)}}}}\advirecord{c32a}{(Mizar)}}
\webad{wiskunde meisjes}{www.wiskundemeisjes.nl}{/}
\adviplay[slidered]{x1}%
\adviplay[slidered]{x2}%
\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}
\adviplay[slidered]{c32}
\adviwait
\adviplay[slideblue]{x1}
\adviplay[slideblue]{x2}
\adviplay[white]{c32}
\adviplay[slidered]{c32a}
\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[slideblue]{c32a}
\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{and a more serious example: \textbf{a demo session in Spain}}
\webad{demos icms}{www.cs.ru.nl/\char`\~freek/demos}{/}
\vspace{-.5em}
\vbox to 0pt{
\vspace{-1em}
\includegraphics[width=110pt]{/home/freek/talks/nmc/pix/demos.\eps}
\vss
}

\begingroup
\leftskip 125pt
\rightskip 0pt
{\textsl{Problem} [{\small B2} from {\small IMO} 1972]}

$f$ and $g$ are real-valued functions defined on the real line.
For all $x$ and $y$,
$$\hspace{120pt} \red{f(x + y) + f(x - y) = 2 f(x) g(y)}.$$
$f$ is not identically zero and \green{$|f(x)| \le 1$ for all $x$}.
Prove that \green{$|g(x)| \le 1$ for all $x$}.

\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch (Isabelle)}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\footnotesize
\advirecord{fx0}{theorem \advirecord{f0c}{IMO}\advirecord{f0d}{:}
  \red{\advirecord{f0a}{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"}}}
\advirecord{fx1}{proof \gray{\advirecord{f9}{(clarify, rule leI, clarify)}}
  \green{\advirecord{f0b}{obtain k where "isLub UNIV \{z. EX x. abs(f x) = z\} k" \blue{\advirecord{f1}{sorry}}
  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))" \blue{\advirecord{f2}{sorry}}
    have "... <= abs(f(x + y)) + abs(f(x - y))" \blue{\advirecord{f3}{sorry}}
    have "... <= 2 * k" \blue{\advirecord{f4}{sorry}}
    show "abs(f x) <= k / abs(g y)" \blue{\advirecord{f5}{sorry}}
  qed
  hence "isUb UNIV \{z. EX x. abs(f x) = z\} (k / abs(g y))" \blue{\advirecord{f6}{sorry}}
  have "k / abs(g y) < k" \blue{\advirecord{f7}{sorry}}
  show False \blue{\advirecord{f8}{sorry}}}}
qed}
\end{alltt}
\endgroup
\adviplay{fx0}
\adviplay[slidegray]{f0c}
\adviplay{f0d}
\adviplay[slidered]{f0a}
\adviwait
\adviplay{fx1}
\adviplay[slidegreen]{f0b}
\adviwait
\adviplay{f0a}
\adviplay{f0b}
\adviplay{f0c}
\adviwait
\adviplay[slidered]{f1}
\adviplay[slidered]{f2}
\adviplay[slidered]{f3}
\adviplay[slidered]{f4}
\adviplay[slidered]{f5}
\adviplay[slidered]{f6}
\adviplay[slidered]{f7}
\adviplay[slidered]{f8}
\adviplay[slidegray]{f9}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{fragment of the full formalization}
\vbox to 0pt{
\vspace{-1.2em}
\def\etcetera{{\sf\textsl{\strut etcetera}}}
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
%theorem IMO:
%  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"
\begin{alltt}\footnotesize
proof \advirecord{d0}{(clarify, rule leI, clarify)}
  obtain k where "isLub UNIV \{z. EX x. abs(f x) = z\} k"
    \red{\advirecord{d1}{by (subgoal_tac "EX k. ?P k", force, insert prems,
        auto intro!: reals_complete isUbI setleI)}}
  \green{\advirecord{d2}{\white{\advirecord{d2b}{\rlap{    have}}}\blue{\advirecord{d2a}{hence a:}} "ALL x. abs(f x) <= k" \red{\advirecord{d3}{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))"
      \red{\advirecord{d4}{by (insert prems, auto simp add: abs_mult)}}
    \blue{\advirecord{d5}{also}} have "... <= abs(f(x + y)) + abs(f(x - y))"
      \red{\advirecord{d6}{by (rule abs_triangle_ineq)}}
    \blue{\advirecord{d7}{also from a}} \green{\advirecord{d8}{have "... <=  k + k"}} \red{\advirecord{d9}{by (intro add_mono, auto)}}
    \blue{\advirecord{d10}{also}} have "... <= 2 * k" \red{\advirecord{d11}{by auto}}
    \blue{\advirecord{d12}{finally}} show "abs(f x) <= k / abs(g y)"
      \red{\advirecord{d13}{by (subst pos_le_divide_eq, insert prems,
          auto simp add: pos_le_divide_eq mult_commute)}}
    \gray{\etcetera}
\end{alltt}
\endgroup
\adviplay[slidegray]{d0}
\adviwait
\adviplay{d0}
\adviplay[slidegreen]{d2}
\adviplay[slidegreen]{d2b}
\adviplay[slidegreen]{d8}
\adviwait
\adviplay[white]{d2b}
\adviplay[slideblue]{d2a}
\adviplay[slideblue]{d5}
\adviplay[slideblue]{d7}
\adviplay[slideblue]{d10}
\adviplay[slideblue]{d12}
\adviwait
\adviplay[slidered]{d1}
\adviplay[slidered]{d3}
\adviplay[slidered]{d4}
\adviplay[slidered]{d6}
\adviplay[slidered]{d9}
\adviplay[slidered]{d11}
\adviplay[slidered]{d13}
\adviwait
\adviplay{d0}
\adviplay{d1}
\adviplay{d2}
\adviplay{d2a}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviplay{d6}
\adviplay{d6}
\adviplay{d7}
\adviplay{d8}
\adviplay{d9}
\adviplay{d10}
\adviplay{d11}
\adviplay{d12}
\adviplay{d13}
\vss
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{is formalization useful?}
\slidetitle{what does it buy me as a mathematician?}
\begin{itemize}
\item[$\bullet$]
\textsl{nothing}

(you will tell the proofs to the computer, not the other way around)
\adviwait
\medskip

\item[$\bullet$]
\red{actually, it \textsl{does} buy you {something}:}
\smallskip

\begin{itemize}
\item
your mathematics will be \textbf{utterly correct}

\item
your mathematics will be \textbf{utterly explicit}

\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{correctness}
\begin{itemize}
\item[$\bullet$]
humans are fallible

\item[$\bullet$]
computer programs always have bugs

\end{itemize}
how can we possibly promise \textbf{utter} correctness?
\adviwait
\bigskip

\textbf{de Bruijn criterion} \\
\red{have a \textbf{very} small \white{\advirecord{g1}{\rlap{program guarantee the correctness}}}\advirecord{g2}{(part of the) program guarantee the correctness}}
\adviplay[slidered]{g1}
\adviwait
\adviplay[white]{g1}
\adviplay[slidered]{g2}
\adviwait
\medskip

\green{HOL Light kernel: 542 lines = 17 pages \\
$+$ proof of correctness of HOL Light kernel has been formalized}
\bigskip
\bigskip
\adviwait

\blue{(but: what if \textbf{definitions} are incorrect{?})}

\vfill
\end{slide}

\begin{slide}
\slidetitle{how difficult is it?}
\textbf{de Bruijn factor}

$$
\phantom{\mbox{\Large $4$} \approx}
{\mbox{size of formalization} \over
\mbox{size of {\LaTeX} source of informal mathematics}}
\adviwait
\approx
\mbox{\Large \red{4}}
\adviwait
\bigskip
\medskip
$$

\blue{de Bruijn factor in time}
$$
{\mbox{time to formalize} \over
\mbox{time to understand the mathematics}}
$$
\blue{is much larger}
\adviwait
\medskip
$$
\mbox{\green{time to formalize one page from a textbook}}
\approx
\mbox{\red{about one week}}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the state of the art: things that have been formalized}
\slidetitle{list of \textbf{100} nice theorems}
\vspace{-1.4em}
\vbox to 0pt{\vspace{-0.76em}
\webad{100 theorems}{www.cs.ru.nl/\char`\~freek/100}{/}
\vss}
\vspace{-1.4em}
\vbox to 0pt{
\vspace{8em}
\gray{\advirecord{h1}{
\hfill\framebox{\parbox{7em}{
\begin{flushright}
\blue{\textsl{formalized:}\hspace{.6em} \textbf{\red{77}}}\\
\smallskip
\black{
{HOL Light\hspace{.6em} 63}\\
\smallskip
Coq\hspace{.6em} 38\\
ProofPower\hspace{.6em} 37\\
Mizar\hspace{.6em} 35\\
Isabelle\hspace{.6em} 33 \\
\smallskip
}
\end{flushright}
}\hspace{3pt}}\hspace{-3em}
}}
\vss
}

\begingroup\footnotesize
\vspace{-3pt}
\begin{flushleft}
\enskip 1. The Irrationality of the Square Root of 2 \\
\enskip 2. Fundamental Theorem of Algebra \\
\enskip 3. The Denumerability of the Rational Numbers \\
\enskip 4. Pythagorean Theorem \\
\enskip 5. Prime Number Theorem \\
\enskip 6. G\"odel's Incompleteness Theorem \\
\enskip 7. Law of Quadratic Reciprocity \\
\enskip 8. The Impossibility of Trisecting the Angle and Doubling the Cube \\
\enskip 9. The Area of a Circle \\
10. Euler's Generalization of Fermat's Little Theorem \\
\enskip\phantom{1. }\dots
\end{flushleft}
\adviwait
\adviplay[slidegray]{h1}
\adviwait
\endgroup

\blue{\textsl{not formalized yet:}}
\begingroup\footnotesize
\begin{flushleft}
12. The Independence of the Parallel Postulate \\
13. Polyhedron Formula \\
\enskip\phantom{1. }\dots
%16. Insolvability of General Higher Degree Equations
\end{flushleft}
\endgroup

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

\begin{slide}
\slidetitle{serious theorems that have been formalized}
\vbox to 0pt{
\vspace{-1em}
\begingroup
\footnotesize
\begin{itemize}
\item[$\bullet$]
\textbf{first incompleteness theorem} \\
nqthm, Natarajan Shankar \\
Coq, Russell O'Connor \\
HOL Light, John Harrison

\item[$\bullet$]
\textbf{fundamental theorem of algebra} \\
Mizar, Robert Milewski \\
HOL Light, John Harrison \\
Coq, Herman Geuvers \& others
\end{itemize}
\endgroup

\begingroup
\small
\begin{itemize}
\item[$\bullet$]
\textbf{Jordan curve theorem} \\
HOL Light, Tom Hales \\
Mizar, Artur Korni{\l}owicz \& others

\item[$\bullet$]
\textbf{prime number theorem} \\
Isabelle, Jeremy Avigad
\end{itemize}
\endgroup

\begin{itemize}
\item[$\bullet$]
\textbf{four color theorem} \\
Coq, Georges Gonthier

\end{itemize}

\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{0.03\% of the four color theorem formalization}
\begin{alltt}\footnotesize
Lemma \gray{unavoidability} : \red{reducibility -> forall g, ~ minimal_counter_example g.}\toolong
Proof.
\green{move=> Hred g Hg; case: (posz_dscore Hg) => x Hx.
step Hgx: valid_hub x by split.
step := (Hg : pentagonal g) x; rewrite 7!leq_eqVlt leqNgt.
rewrite exclude5 ?exclude6 ?exclude7 ?exclude8 ?exclude9 ?exclude10 ?exclude11 //.\toolong
case/idP; apply: (@dscore_cap1 g 5) => {x n Hn Hx Hgx}// y.
pose x := inv_face2 y; pose n := arity x.
step ->: y = face (face x) by rewrite /x /inv_face2 !Enode.
rewrite (dbound1_eq (DruleFork (DruleForkValues n))) // leqz_nat.
case Hn: (negb (Pr58 n)); first by rewrite source_drules_range //.
step Hrp := no_fit_the_redpart Hred Hg.
apply: (check_dbound1P (Hrp the_quiz_tree) _ (exact_fitp_pcons_ Hg x)) => //.\toolong
rewrite -/n; move: n Hn; do 9 case=> //.}
Qed.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the state of the art: the four best systems}
\slidetitle{proof assistants for mathematics}
\vspace{-1.4em}
\vbox to 0pt{\vspace{-0.76em}
\webad{provers}{www.cs.ru.nl/\char`\~freek/comparison}{/}
\vspace{16em}
\footnotesize
\green{\advirecord{b1}{%
\textsl{$\!$The Seventeen Provers of the World} \\
Lecture Notes in Artificial Intelligence 3600
}}
\vss}
\begin{center}
\medskip
\setlength{\unitlength}{.6mm}
\hspace{0em}\begin{picture}(110,91)(-20,-1)
\thinlines\footnotesize
\gray{\advirecord{i1}{\put(-20,90){\circle*{4}}}}\red{\advirecord{i2}{\put(-20,86.5){\makebox(0,0)[rt]{nqthm}}\put(-20,82){\makebox(0,0)[rt]{ACL2}}}}
\gray{\advirecord{i3}{\put(42,80){\circle*{4}}}}\red{\advirecord{i4}{\put(38.5,82){\makebox(0,0)[r]{PVS}}}}
\advirecord{i5}{\put(74,74){\circle*{6}}}\red{\advirecord{i6}{\put(78.5,75){\makebox(0,0)[lt]{Isabelle}}}}
\advirecord{i7}{\put(62,72){\circle*{8}}}\red{\advirecord{i8}{\put(59,86.5){\makebox(0,0)[cb]{HOL4}}\put(59,82.5){\makebox(0,0)[cb]{ProofPower}}}\advirecord{i9}{\put(59,77.5){\makebox(0,0)[cb]{HOL$\,$Light}}}}
\gray{\advirecord{i10}{\put(54,70){\circle*{2}}}}\red{\advirecord{i11}{\put(54,68.5){\makebox(0,0)[rt]{$\Omega$mega}}}}
\gray{\advirecord{i12}{\put(16,68){\circle*{2}}}}\red{\advirecord{i13}{\put(14.5,71.5){\makebox(0,0)[r]{Otter}}}}
\gray{\advirecord{i14}{\put(20,66){\circle*{2}}}}\red{\advirecord{i15}{\put(19,65){\makebox(0,0)[rt]{Theorema}}}}
\gray{\advirecord{i16}{\put(24,62){\circle*{2}}}}\red{\advirecord{i17}{\put(26,59.5){\makebox(0,0)[ct]{IMPS}}}}
\gray{\advirecord{i18}{\put(70,60){\circle*{4}}}}\red{\advirecord{i19}{\put(68.5,57.5){\makebox(0,0)[rt]{NuPRL}}\put(68.5,53.5){\makebox(0,0)[rt]{MetaPRL}}}}
\advirecord{i20}{\put(78,58){\circle*{6}}}\red{\advirecord{i21}{\put(82,55){\makebox(0,0)[l]{Coq}}}}
\gray{\advirecord{i22}{\put(58,41){\circle*{2}}}}\red{\advirecord{i23}{\put(56.5,40){\makebox(0,0)[rt]{PhoX}}}}
\gray{\advirecord{i24}{\put(82,39){\circle*{2}}}}\red{\advirecord{i25}{\put(82,37){\makebox(0,0)[lt]{Lego}}\put(82,32.5){\makebox(0,0)[lt]{Epigram}}}}
\advirecord{i26}{\put(66,10){\circle*{6}}}\red{\advirecord{i27}{\put(62,9){\makebox(0,0)[rt]{Mizar}}}}
\gray{\advirecord{i28}{\put(86,1){\circle*{2}}}}\red{\advirecord{i29}{\put(85,0){\makebox(0,0)[rt]{Agda}}}}
\gray{\advirecord{i30}{\put(90,-1){\circle*{2}}}}\red{\advirecord{i31}{\put(90,-3.5){\makebox(0,0)[lt]{Metamath}}}}
\end{picture}
\end{center}
\adviplay{i1}
\adviplay{i3}
\adviplay{i5}
\adviplay{i7}
\adviplay{i10}
\adviplay{i12}
\adviplay{i14}
\adviplay{i16}
\adviplay{i18}
\adviplay{i20}
\adviplay{i22}
\adviplay{i24}
\adviplay{i26}
\adviplay{i28}
\adviplay{i30}
\adviwait
\adviplay[slidered]{i2}
\adviplay[slidered]{i4}
\adviplay[slidered]{i6}
\adviplay[slidered]{i8}
\adviplay[slidered]{i9}
\adviplay[slidered]{i11}
\adviplay[slidered]{i13}
\adviplay[slidered]{i15}
\adviplay[slidered]{i17}
\adviplay[slidered]{i19}
\adviplay[slidered]{i21}
\adviplay[slidered]{i23}
\adviplay[slidered]{i25}
\adviplay[slidered]{i27}
\adviplay[slidered]{i29}
\adviplay[slidered]{i31}
\adviwait
\adviplay[slidegreen]{b1}
\adviwait
\adviplay[white]{i1}
\adviplay[white]{i2}
\adviplay[white]{i3}
\adviplay[white]{i4}
\adviplay[white]{i8}
\adviplay[white]{i10}
\adviplay[white]{i11}
\adviplay[white]{i12}
\adviplay[white]{i13}
\adviplay[white]{i14}
\adviplay[white]{i15}
\adviplay[white]{i16}
\adviplay[white]{i17}
\adviplay[white]{i18}
\adviplay[white]{i19}
\adviplay[white]{i22}
\adviplay[white]{i23}
\adviplay[white]{i24}
\adviplay[white]{i25}
\adviplay[white]{i28}
\adviplay[white]{i29}
\adviplay[white]{i30}
\adviplay[white]{i31}

\vfill
\end{slide}

\begin{slide}
\slidetitle{first system: \textbf{{HOL} Light}}
John Harrison, University of Cambridge $\leadsto$ Intel Corporation \hfill
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/uk.\eps}$\,$%
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/usa.\eps}%
\medskip

\begin{tabular}{rl}
\textbf{advantages} & very elegant system \\
\noalign{\vspace{-\smallskipamount}}
& strong automation \\
\textbf{disadvantages} & not really well suited for abstract algebra \\
\noalign{\vspace{-\smallskipamount}}
& \blue{\advirecord{j1}{unreadable proof scripts}}\adviplay{j1}
\end{tabular}
\adviwait
\adviplay[slideblue]{j1}
\bigskip

\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
let \gray{LEMMA1} = prove
 (`\red{(!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\\ (!x. abs(f x) <= &1)\toolong
   ==> !l x. abs(f x * (g y) pow l) <= &1}`,
  \green{DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN INDUCT_TAC THEN
  ASM_SIMP_TAC[real_pow; REAL_MUL_RID] THEN GEN_TAC THEN MATCH_MP_TAC
   (REAL_ARITH `abs((&2 * a * b) * c) <= &2 ==> abs(a * b * c) <= &1`) THEN\toolong
  ASM_SIMP_TAC[] THEN FIRST_ASSUM(MP_TAC o SPEC `x + y`) THEN
  FIRST_ASSUM(MP_TAC o SPEC `x - y`) THEN REAL_ARITH_TAC});;
\end{alltt}
\endgroup

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

\begin{slide}
\slidetitle{second system: \textbf{Mizar}}
Andrzej Trybulec, Bia\l ystok, Poland\hfill
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/poland.\eps}%
\medskip

\begin{tabular}{rl}
\textbf{advantages} & \blue{\advirecord{k1}{readable proof scripts}}\adviplay{k1} \\
\noalign{\vspace{-\smallskipamount}}
& closest to actual mathematics \\
\textbf{disadvantages} & no first class binders (limits, sums, integrals) \\
\noalign{\vspace{-\smallskipamount}}
& no user automation
\end{tabular}
\adviwait
\adviplay[slideblue]{k1}
\bigskip
\medskip

\begingroup
\vbox to 0pt{
\begingroup
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\hfill
\blue{
\begin{picture}(5,5)
\put(0.5,4.5){\makebox(0,0){\lightgray{\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[slideblue]{e0}
\end{picture}
}
\endgroup
\vss
}
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slideblue]{e0}%

\vspace{-1.5em}
\begin{itemize}
\item[$\bullet$]
\textsl{procedural} \\
\green{HOL Light, Coq, Isabelle} \\
\begingroup
\small
\blue{%
\adviwait
\adviplay[slidelightgray]{e17}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e17}%
E
\adviplay[slidelightgray]{e16}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e16}%
E
\adviplay[slidelightgray]{e15}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e15}%
S
\adviplay[slidelightgray]{e14}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e14}%
E
\adviplay[slidelightgray]{e13}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e13}%
N
\adviplay[slidelightgray]{e12}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e12}%
E
\adviplay[slidelightgray]{e11}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e11}%
S
\adviplay[slidelightgray]{e10}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e10}%
S
\adviplay[slidelightgray]{e9}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e9}%
S
\adviplay[slidelightgray]{e8}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e8}%
W
\adviplay[slidelightgray]{e7}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e7}%
W
\adviplay[slidelightgray]{e6}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e6}%
W
\adviplay[slidelightgray]{e5}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e5}%
S
\adviplay[slidelightgray]{e4}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e4}%
E
\adviplay[slidelightgray]{e3}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e3}%
E
\adviplay[slidelightgray]{e2}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e2}%
E
\adviplay[slidelightgray]{e1}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slideblue]{e0}
}
\endgroup

%\adviwait
\item[$\bullet$]
\textsl{declarative} \\
\green{Mizar, Isabelle}
\vspace{-.3\smallskipamount} \\
\begingroup
\scriptsize
\blue{
\adviwait
(0,0)
\adviplay[slidelightgray]{e1}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e1}%
(1,0)
\adviplay[slidelightgray]{e2}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e2}%
(2,0)
\adviplay[slidelightgray]{e3}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e3}%
(3,0)
\adviplay[slidelightgray]{e4}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e4}%
(3,1)
\adviplay[slidelightgray]{e5}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e5}%
(2,1)
\adviplay[slidelightgray]{e6}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e6}%
(1,1)
\adviplay[slidelightgray]{e7}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e7}%
(0,1)
\adviplay[slidelightgray]{e8}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e8}%
(0,2)
\adviplay[slidelightgray]{e9}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e9}%
(0,3)
\adviplay[slidelightgray]{e10}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e10}%
(0,4)
\adviplay[slidelightgray]{e11}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e11}%
(1,4)
\adviplay[slidelightgray]{e12}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e12}%
(1,3)
\adviplay[slidelightgray]{e13}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e13}%
(2,3)
\adviplay[slidelightgray]{e14}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e14}%
(2,4)
\adviplay[slidelightgray]{e15}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e15}%
(3,4)
\adviplay[slidelightgray]{e16}\adviplay[slideblue]{e0}\adviwait\adviplay[white]{e16}%
(4,4)
\adviplay[slidelightgray]{e17}\adviplay[slideblue]{e0}%\adviwait\adviplay[white]{e17}%
\adviplay[slideblue]{e0}%
}\toolong
\endgroup

\end{itemize}
\endgroup

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

\begin{slide}
\slidetitle{third system: \textbf{Isabelle}}
Larry Paulson, University of Cambridge \hfill
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/uk.\eps}\\
Tobias Nipkow \& Makarius Wenzel, Technical University Munich \hfill
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/germany.\eps}$\hspace{.7pt}$%
\medskip

\begin{tabular}{rl}
\textbf{advantages} & automation like HOL Light \\
\noalign{\vspace{-\smallskipamount}}
& readable like Mizar \\
\textbf{disadvantage} & \advirecord{l1}{not really well suited for abstract algebra}\adviplay{l1}
\end{tabular}
\adviwait
\adviplay[slideblue]{l1}
\bigskip

\begin{itemize}
\item[$\bullet$]
\textsl{set theory} (`ZFC')

\item[$\bullet$]
\textsl{type theory} $\leadsto$ each object has a `type'

{recursion/induction hardwired into the foundations}

\item[$\bullet$]
\blue{\textsl{higher order logic}} = weak set theory, also typed 

\green{very simple and elegant \\
not as expressive as set theory and type theory}
\end{itemize}

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

\begin{slide}
\slidetitle{fourth system: \textbf{Coq}}
\webad{intuitionism questions}{www.intuitionism.org}{/}
G\'erard Huet \& Thierry Coquand \& many others, {\small INRIA}, Paris \hfill
\includegraphics[width=16pt]{/home/freek/talks/nmc/pix/flags/france.\eps}%
\medskip

\begin{tabular}{rl}
\textbf{advantages} & automation like HOL Light and Isabelle \\
\noalign{\vspace{-\smallskipamount}}
& expressive like Mizar \\
\textbf{disadvantages} & baroque foundations \\
\noalign{\vspace{-\smallskipamount}}
& \advirecord{m1}{designed for intuitionistic mathematics}\adviplay{m1}
\end{tabular}
\adviwait
\adviplay[slideblue]{m1}
\bigskip

\green{intermediate value theorem is intuitionistically not valid}
\medskip
\begin{flushright}
\begin{picture}(90,60)(-10,-10)
\gray{
\put(0,-10){\line(0,1){60}}
\put(70,-10){\line(0,1){60}}
\put(0,-12){\makebox(0,0)[tc]{$a$}}
\put(70,-12){\makebox(0,0)[tc]{$b$}}
}
\put(0,20){\line(1,0){70}}
\thinlines
\red{
\put(0,0){\line(1,1){20}}
\put(20,20){\line(1,0){30}}
\put(50,20){\line(1,1){20}}
\put(36,23){\makebox(0,0)[cb]{$f$}}
}
\end{picture}
\end{flushright}

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

\begin{slide}
\sectiontitle{the state of the art: current projects}
\slidetitle{flyspeck}
\vspace{-1em}
\vbox to 0pt{
\vspace{-1.1em}
\hfill\includegraphics[width=9em]{/home/freek/talks/nmc/pix/kepler.\eps}%
$\hspace{-.5pt}$
\vss
}
\begin{quote}
\blue{\textsl{FlysPecK = Formal Proof of Kepler}}\adviwait
\end{quote}
\medskip

Tom Hales' proof of Kepler's conjecture: \\
\green{3 gigabytes of computer programs and data}
\medskip
\smallskip

\adviwait
\red{referees did not understand it}
\begin{itemize}
\item[$\bullet$]
`normal part' published in the \textsl{Annals of Mathematics}
\item[$\bullet$]
`computer part' published in \textsl{Discrete and Computational Geometry}
\end{itemize}
\adviwait
\bigskip
\vspace{-\smallskipamount}

{2003: flyspeck project} $\leadsto$ \red{convincing the world} \\
\blue{various prover communities involved: HOL Light, Coq, Isabelle}

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

\begin{slide}
\slidetitle{the microsoft/{\small INRIA} institute}
the three theorems everyone always starts talking about:
\begin{itemize}
\item[$\bullet$]
\strut\advirecord{n2}{\rlap{\textsl{\st{four color theorem}}}}\advirecord{n3}{\textsl{four color theorem}}\adviplay{n3}\ 

\green{\advirecord{n4}{Georges Gonthier, 2004}}\ 

\item[$\bullet$]
\textsl{Fermat's last theorem}

\green{\advirecord{n5}{probably too big a hurdle yet$\,$\dots}}

\item[$\bullet$]
\advirecord{n1}{\textsl{classification of finite simple groups}}\adviplay{n1}

\end{itemize}
\adviwait
\adviplay[white]{n3}\adviplay{n2}\adviplay[slidegreen]{n4}
\adviwait
\adviplay[slidegreen]{n5}
\adviwait
%\adviplay[slidered]{n1}
\medskip

Georges Gonthier now has started work on the \\
\textbf{odd order theorem = \red{Feit-Thompson theorem}}
\smallskip

\begin{quote}
\small
\textsl{%
It takes a professional group theorist about a year of hard work to understand the proof completely} [$\,$\dots]
\\
\strut\hfill --- Wikipedia
\end{quote}

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

\begin{slide}
\sectiontitle{outlook}
\slidetitle{two common misunderstandings}
\begin{itemize}
\item[$\bullet$]
\textbf{this will never be big: formalization is just too much work}
%\medskip

\blue{misunderstanding:} \red{underestimating technology}
\medskip

\begingroup
\footnotesize
%[$\,$\dots]
\textsl{%
After formalizing the prime number theorem, I was struck with near
certainty that,
within a few decades, formally verified mathematics will
become the norm.}
[$\,$\dots]
\textsl{there are no
major conceptual hurdles that need to be overcome;
all it will take is
clear thinking, sound engineering, and hard work.
}
%[$\,$\dots]
\\
\strut\hfill --- Jeremy Avigad
\medskip
\adviwait

\endgroup
\item[$\bullet$]
\textbf{`I know mathematics, I can do this much better'}
\smallskip

\begingroup\footnotesize
Paul Cohen,
Harvey Friedman,
Arnold Neumaier,
\textsl{etcetera}

\endgroup
\medskip

\blue{misunderstanding:} \red{image of the computer as a research assistant} %that you can talk to

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the best computer game in the world}
formalization is like
\medskip
\begin{itemize}
\item[$\bullet$]
\textbf{programming} \\
\green{but no bugs, and not as trivial}

\item[$\bullet$]
\textbf{doing mathematics} \\
\green{but completely transparent, and the computer helps}

\end{itemize}
\adviwait
\medskip
\smallskip

if you don't like one of them, you won't like formalization \\
\red{if you like both, you will like formalization \textbf{very} much}
\bigskip

\begin{quote}
\small
\textsl{%
Coq proofs are developed interactively} [$\,$\dots]
\textsl{%
%using a number of
%tactics as elementary proof steps.
%The sequence of tactics used constitutes the proof script.
Building such scripts \blue{is surprisingly addictive, in a videogame
kind of way}} [$\,$\dots] \\
\strut\hfill --- Xavier Leroy
\end{quote}

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

\begin{slide}
\slidetitle{the three revolutions in mathematics}
\begin{itemize}
\item[{$\bullet$}]
{ancient greeks:}

\textbf{proof}
\medskip

\item[{$\bullet$}]
{end nineteenth century:}

\textbf{rigor}
\medskip

\item[{$\bullet$}]
{start twenty-first century:}

%\textbf{\red{complete detail}}
\textbf{\red{formalization of mathematics}}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{will formalization become commonplace?}
\green{`killer app' for formalization has not yet been found}$\,$\dots
\adviwait
\medskip
\smallskip

current technology already very attractive:
\begin{itemize}
\item[$\bullet$]
mathematics that is \textbf{utterly correct}

\item[$\bullet$]
mathematics that is \textbf{utterly explicit}

\end{itemize}
\adviwait
\bigskip
\bigskip

\textbf{\red{things will really become interesting when:}}
\vspace{-1.8\bigskipamount}

\begingroup
\large
$$\red{\hspace{1em}\mbox{\normalsize\textsl{time needed for formalization}} \mathrel{{<}} \mbox{\rlap{\white{\advirecord{o1}{\normalsize\textsl{time needed for referee checking}}}\adviplay[slidered]{o1}\adviwait\adviplay[white]{o1}}}3 \cdot \mbox{\normalsize\textsl{time needed for referee checking}}}$$
\endgroup

\vfill
\end{slide}

\end{document}