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

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

\setcounter{slide}{-1}
\begin{slide}
\strut\vspace{2em}

\slidetitle{\Large\strut statistics on digital libraries of mathematics}

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

\red{{\small MKM 2008}} \\
{\small CICM 2008}, Birmingham, UK \\
{\small 2008\hspace{3pt}06\hspace{3pt}28, 12\hspace{1pt}:\hspace{1.8pt}00}
\vspace{2.5em}
\adviwait

\gray{\fbox{\hspace{-3.4pt}\hbox to \hsize{\small\hspace{3pt}\begin{tabular}{l}\green{\texttt{http://www.cs.ru.nl/\char`\~freek/}}\red{\texttt{notes/stats.pdf}}\\\noalign{\vspace{-.5\smallskipamount}}\green{\texttt{http://www.cs.ru.nl/\char`\~freek/}}\red{\texttt{talks/stats.pdf}}\\\noalign{\smallskip}\end{tabular}\hss}\hspace{-3.4pt}}}
\vspace{-1em}

\end{slide}

\begin{slide}
\slidetitle{libraries of mathematics}
\begin{itemize}
\item[$\bullet$]
\textbf{text}
\begin{itemize}
\item
\smallskip
paper \\
\green{journals, textbooks}
\adviwait
\smallskip

\item
electrons \\
\green{archives, websites}

\end{itemize}
\adviwait
\medskip

\item[$\bullet$]
\textbf{code}
\smallskip
\begin{itemize}
\item
mathematical tables
\smallskip

\item
software \\
\green{numerical, computer algebra, subject specific}
\smallskip

\item
\red{\advirecord{a}{formalizations}}
\adviplay{a}
\adviwait
\adviplay[slidered]{a}

\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{80 out of \green{\advirecord{g}{100 theorems}}\adviplay[slideblue]{g}}
\vbox to 0pt{\small
\vspace{-1.1em}
\begin{tabular}{lr}
\enskip 1. The Irrationality of the Square Root of 2 & \llap{$\ge {\sf 17}$} \\
\enskip 2. \red{Fundamental Theorem of Algebra} & 4 \\
\enskip 3. The Denumerability of the Rational Numbers & 6 \\
\enskip 4. Pythagorean Theorem & 6 \\
\enskip 5. \red{Prime Number Theorem} & 2 \\
\enskip 6. \red{G\"odel's Incompleteness Theorem} & 3 \\
\enskip 7. Law of Quadratic Reciprocity & 4 \\
\enskip 8. The Impossibility of Trisecting the Angle and Doubling the Cube$\quad$ & 1 \\
\enskip 9. The Area of a Circle & 1 \\
10. Euler's Generalization of Fermat's Little Theorem & 4 \\
11. The Infinitude of Primes & 6 \\
12. \green{The Independence of the Parallel Postulate} & \green{0} \\
13. \red{Polyhedron Formula} & 1 \\
\phantom{00. }\dots
\end{tabular}
\vss
}
\adviwait
\adviplay[slidegreen]{g}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof assistants}

{only \red{five systems} seriously used \green{for mathematics}}
\bigskip
\medskip

\begin{center}
\quad
\begin{tabular}{llcr}
\llap{\setbox0=\hbox{{\advirecord{b3}{$\mbox{\small HOL}\;\Bigg\{\quad\quad$}}}\ht0=-1em\dp0=-1em\raise -.92em\box0}%
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}$\quad\quad$ &
\textbf{{\small HOL} Light} &$\hspace{5em}$& 69 \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps} &
\gray{\textbf{\advirecord{b1}{ProofPower}}}\adviplay{b1} && \gray{\advirecord{b2}{42}}\adviplay{b2} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/germany.eps} &
\textbf{Isabelle} && 40 \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/france.eps} &
\textbf{Coq} && 39 \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/poland.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/japan.eps} &
\textbf{Mizar} && 45
\end{tabular}
\end{center}
\adviwait
\adviplay{b3}
\adviwait
\adviplay[slidelightgray]{b1}
\adviplay[slidelightgray]{b2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{library sizes}
\begin{center}
\vbox to 0pt{
\includegraphics[height=18em]{/home/freek/talks/stats/sizes.eps}
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{content of the files}

{formalization} $\enskip\approx\enskip$ \blue{long chain of \textbf{lemmas}}
\bigskip
\medskip
%\adviwait

\blue{lemma} $\enskip\approx\enskip$
\smallskip
\begin{itemize}
\item[]
\red{label} $\enskip+\enskip$

\item[]
\red{statement} $\enskip+\enskip$

\item[]
\textbf{\green{proof}}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\small HOL} Light sample\hfill\blue{\footnotesize\texttt{Examples/binary.ml}}}
\vbox to 0pt{
\vspace{-1.1em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\scriptsize
\gray{\advirecord{c1a}{C} \advirecord{c1b}{(* ========================================================================= *)}
\advirecord{c2a}{C} \advirecord{c2b}{(* Binary expansions as a bijection between numbers and finite sets.         *)}
\advirecord{c3a}{C} \advirecord{c3b}{(* ========================================================================= *)}
\advirecord{c4a}{B}}
\red{\advirecord{c5a}{T} \advirecord{c5b}{let LT_POW2_REFL = prove}
\advirecord{c6a}{T} \advirecord{c6b}{ (`!n. n < 2 EXP n`,}}
\green{\advirecord{c7a}{P} \advirecord{c7b}{  INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);;}}
\gray{\advirecord{c8a}{B}}
\red{\advirecord{c9a}{T} \advirecord{c9b}{let BINARY_INDUCT = prove}
\advirecord{c10a}{T} \advirecord{c10b}{ (`!P. P 0 /\\ (!n. P n ==> P(2 * n) /\\ P(2 * n + 1)) ==> !n. P n`,}}
\green{\advirecord{c11a}{P} \advirecord{c11b}{  GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN GEN_TAC THEN}
\advirecord{c12a}{P} \advirecord{c12b}{  STRIP_ASSUME_TAC(ARITH_RULE}
\advirecord{c13a}{P} \advirecord{c13b}{   `n = 0 \\/ n DIV 2 < n /\\ (n = 2 * n DIV 2 \\/ n = 2 * n DIV 2 + 1)`) THEN}
\advirecord{c14a}{P} \advirecord{c14b}{  ASM_MESON_TAC[]);;}}
\gray{\advirecord{c15a}{B}}
\red{\advirecord{c16a}{T} \advirecord{c16b}{let BOUNDED_FINITE = prove}
\advirecord{c17a}{T} \advirecord{c17b}{ (`!s. (!x:num. x IN s ==> x <= n) ==> FINITE s`,}}
\green{\advirecord{c18a}{P} \advirecord{c18b}{  REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN}
\advirecord{c19a}{P} \advirecord{c19b}{  ASM_SIMP_TAC[SUBSET; IN_NUMSEG; FINITE_NUMSEG; LE_0]);;}}
\gray{\advirecord{c20a}{B}}
\red{\advirecord{c21a}{T} \advirecord{c21b}{let EVEN_NSUM = prove}
\advirecord{c22a}{T} \advirecord{c22b}{ (`!s. FINITE s /\\ (!i. i IN s ==> EVEN(f i)) ==> EVEN(nsum s f)`,}}
\green{\advirecord{c23a}{P} \advirecord{c23b}{  REWRITE_TAC[GSYM IMP_IMP] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN}}
\end{alltt}
\endgroup
\vss}
\adviplay{c1b}
\adviplay{c2b}
\adviplay{c3b}
\adviplay{c5b}
\adviplay{c6b}
\adviplay{c7b}
\adviplay{c9b}
\adviplay{c10b}
\adviplay{c11b}
\adviplay{c12b}
\adviplay{c13b}
\adviplay{c14b}
\adviplay{c16b}
\adviplay{c17b}
\adviplay{c18b}
\adviplay{c19b}
\adviplay{c21b}
\adviplay{c22b}
\adviplay{c23b}
\adviwait
\adviplay[slideblue]{c1a}
\adviplay[slideblue]{c2a}
\adviplay[slideblue]{c3a}
\adviplay[slideblue]{c4a}
\adviplay[slideblue]{c5a}
\adviplay[slideblue]{c6a}
\adviplay[slideblue]{c7a}
\adviplay[slideblue]{c8a}
\adviplay[slideblue]{c9a}
\adviplay[slideblue]{c10a}
\adviplay[slideblue]{c11a}
\adviplay[slideblue]{c12a}
\adviplay[slideblue]{c13a}
\adviplay[slideblue]{c14a}
\adviplay[slideblue]{c15a}
\adviplay[slideblue]{c16a}
\adviplay[slideblue]{c17a}
\adviplay[slideblue]{c18a}
\adviplay[slideblue]{c19a}
\adviplay[slideblue]{c20a}
\adviplay[slideblue]{c21a}
\adviplay[slideblue]{c22a}
\adviplay[slideblue]{c23a}
\adviwait
\adviplay[slidegray]{c1a}
\adviplay[slidegray]{c1b}
\adviplay[slidegray]{c2a}
\adviplay[slidegray]{c2b}
\adviplay[slidegray]{c3a}
\adviplay[slidegray]{c3b}
\adviplay[slidegray]{c4a}
\adviplay[slidered]{c5a}
\adviplay[slidered]{c5b}
\adviplay[slidered]{c6a}
\adviplay[slidered]{c6b}
\adviplay[slidegreen]{c7a}
\adviplay[slidegreen]{c7b}
\adviplay[slidegray]{c8a}
\adviplay[slidered]{c9a}
\adviplay[slidered]{c9b}
\adviplay[slidered]{c10a}
\adviplay[slidered]{c10b}
\adviplay[slidegreen]{c11a}
\adviplay[slidegreen]{c11b}
\adviplay[slidegreen]{c12a}
\adviplay[slidegreen]{c12b}
\adviplay[slidegreen]{c13a}
\adviplay[slidegreen]{c13b}
\adviplay[slidegreen]{c14a}
\adviplay[slidegreen]{c14b}
\adviplay[slidegray]{c15a}
\adviplay[slidered]{c16a}
\adviplay[slidered]{c16b}
\adviplay[slidered]{c17a}
\adviplay[slidered]{c17b}
\adviplay[slidegreen]{c18a}
\adviplay[slidegreen]{c18b}
\adviplay[slidegreen]{c19a}
\adviplay[slidegreen]{c19b}
\adviplay[slidegray]{c20a}
\adviplay[slidered]{c21a}
\adviplay[slidered]{c21b}
\adviplay[slidered]{c22a}
\adviplay[slidered]{c22b}
\adviplay[slidegreen]{c23a}
\adviplay[slidegreen]{c23b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Isabelle sample\hfill\blue{\footnotesize\texttt{HOL/NumberTheory/Int2.thy}}}
\vbox to 0pt{
\vspace{-1.1em}
\begingroup
\def\\{\char`\\}
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\scriptsize
\gray{\advirecord{d1a}{C} \advirecord{d1b}{(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy}
\advirecord{d2a}{C} \advirecord{d2b}{    ID:         $Id: Int2.thy,v 1.12 2007/06/11 09:06:07 chaieb Exp $}
\advirecord{d3a}{C} \advirecord{d3b}{    Authors:    Jeremy Avigad, David Gray, and Adam Kramer}
\advirecord{d4a}{C} \advirecord{d4b}{*)}
\advirecord{d5a}{B}
\advirecord{d6a}{E} \advirecord{d6b}{header \{*Integers: Divisibility and Congruences*\}}
\advirecord{d7a}{B}}
\advirecord{d8a}{S} \advirecord{d8b}{theory Int2 imports Finite2 WilsonRuss begin}
\gray{\advirecord{d9a}{B}}
\blue{\advirecord{d10a}{D} \advirecord{d10b}{definition}
\advirecord{d11a}{D} \advirecord{d11b}{  MultInv :: "int => int => int" where}
\advirecord{d12a}{D} \advirecord{d12b}{  "MultInv p x = x ^ nat (p - 2)"}}
\gray{\advirecord{d13a}{B}
\advirecord{d14a}{B}
\advirecord{d15a}{E} \advirecord{d15b}{subsection \{* Useful lemmas about dvd and powers *\}}
\advirecord{d16a}{B}}
\red{\advirecord{d17a}{T} \advirecord{d17b}{lemma zpower_zdvd_prop1:}
\advirecord{d18a}{T} \advirecord{d18b}{  "0 < n \\<Longrightarrow> p dvd y \\<Longrightarrow> p dvd ((y::int) ^ n)"}}
\green{\advirecord{d19a}{P} \advirecord{d19b}{  by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])}}
\gray{\advirecord{d20a}{B}}
\red{\advirecord{d21a}{T} \advirecord{d21b}{lemma zdvd_bounds: "n dvd m ==> m \\<le> (0::int) | n \\<le> m"}}
\green{\advirecord{d22a}{P} \advirecord{d22b}{proof -}
\advirecord{d23a}{P} \advirecord{d23b}{  assume "n dvd m"}}
\end{alltt}
\endgroup
\vss}
\adviplay{d1b}
\adviplay{d2b}
\adviplay{d3b}
\adviplay{d4b}
\adviplay{d6b}
\adviplay{d8b}
\adviplay{d10b}
\adviplay{d11b}
\adviplay{d12b}
\adviplay{d15b}
\adviplay{d17b}
\adviplay{d18b}
\adviplay{d19b}
\adviplay{d21b}
\adviplay{d22b}
\adviplay{d23b}
\adviwait
\adviplay[slideblue]{d1a}
\adviplay[slideblue]{d2a}
\adviplay[slideblue]{d3a}
\adviplay[slideblue]{d4a}
\adviplay[slideblue]{d5a}
\adviplay[slideblue]{d6a}
\adviplay[slideblue]{d7a}
\adviplay[slideblue]{d8a}
\adviplay[slideblue]{d9a}
\adviplay[slideblue]{d10a}
\adviplay[slideblue]{d11a}
\adviplay[slideblue]{d12a}
\adviplay[slideblue]{d13a}
\adviplay[slideblue]{d14a}
\adviplay[slideblue]{d15a}
\adviplay[slideblue]{d16a}
\adviplay[slideblue]{d17a}
\adviplay[slideblue]{d18a}
\adviplay[slideblue]{d19a}
\adviplay[slideblue]{d20a}
\adviplay[slideblue]{d21a}
\adviplay[slideblue]{d22a}
\adviplay[slideblue]{d23a}
\adviwait
\adviplay[slidegray]{d1a}
\adviplay[slidegray]{d1b}
\adviplay[slidegray]{d2a}
\adviplay[slidegray]{d2b}
\adviplay[slidegray]{d3a}
\adviplay[slidegray]{d3b}
\adviplay[slidegray]{d4a}
\adviplay[slidegray]{d4b}
\adviplay[slidegray]{d5a}
\adviplay[slidegray]{d6a}
\adviplay[slidegray]{d6b}
\adviplay[slidegray]{d7a}
\adviplay{d8a}
\adviplay[slidegray]{d9a}
\adviplay[slideblue]{d10a}
\adviplay[slideblue]{d10b}
\adviplay[slideblue]{d11a}
\adviplay[slideblue]{d11b}
\adviplay[slideblue]{d12a}
\adviplay[slideblue]{d12b}
\adviplay[slidegray]{d13a}
\adviplay[slidegray]{d14a}
\adviplay[slidegray]{d15a}
\adviplay[slidegray]{d15b}
\adviplay[slidegray]{d16a}
\adviplay[slidered]{d17a}
\adviplay[slidered]{d17b}
\adviplay[slidered]{d18a}
\adviplay[slidered]{d18b}
\adviplay[slidegreen]{d19a}
\adviplay[slidegreen]{d19b}
\adviplay[slidegray]{d20a}
\adviplay[slidered]{d21a}
\adviplay[slidered]{d21b}
\adviplay[slidegreen]{d22a}
\adviplay[slidegreen]{d22b}
\adviplay[slidegreen]{d23a}
\adviplay[slidegreen]{d23b}

\vfill
\end{slide}


\begin{slide}
\slidetitle{Coq sample\hfill\blue{\footnotesize\texttt{Logic/Decidable.v}}}
\vbox to 0pt{
\vspace{-1.1em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\scriptsize
\gray{\advirecord{e1a}{C} \advirecord{e1b}{(************************************************************************)}
\advirecord{e2a}{C} \advirecord{e2b}{(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)}
\advirecord{e3a}{C} \advirecord{e3b}{(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)}
\advirecord{e4a}{C} \advirecord{e4b}{(*   \\VV/  **************************************************************)}
\advirecord{e5a}{C} \advirecord{e5b}{(*    //   *      This file is distributed under the terms of the       *)}
\advirecord{e6a}{C} \advirecord{e6b}{(*         *       GNU Lesser General Public License Version 2.1        *)}
\advirecord{e7a}{C} \advirecord{e7b}{(************************************************************************)}
\advirecord{e8a}{C} \advirecord{e8b}{(*i     $Id: Decidable.v 5920 2004-07-16 20:01:26Z herbelin $    i*)}
\advirecord{e9a}{B}
\advirecord{e10a}{E} \advirecord{e10b}{(** Properties of decidable propositions *)}
\advirecord{e11a}{B}}
\blue{\advirecord{e12a}{D} \advirecord{e12b}{Definition decidable (P:Prop) := P \\/ ~ P.}}
\gray{\advirecord{e13a}{B}}
\red{\advirecord{e14a}{T} \advirecord{e14b}{Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P.}}
\green{\advirecord{e15a}{P} \advirecord{e15b}{unfold decidable in |- *; tauto.}
\advirecord{e16a}{P} \advirecord{e16b}{Qed.}}
\gray{\advirecord{e17a}{B}}
\red{\advirecord{e18a}{T} \advirecord{e18b}{Theorem dec_True : decidable True.}}
\green{\advirecord{e19a}{P} \advirecord{e19b}{unfold decidable in |- *; auto.}
\advirecord{e20a}{P} \advirecord{e20b}{Qed.}}
\gray{\advirecord{e21a}{B}}
\red{\advirecord{e22a}{T} \advirecord{e22b}{Theorem dec_False : decidable False.}}
\green{\advirecord{e23a}{P} \advirecord{e23b}{unfold decidable, not in |- *; auto.}}
\end{alltt}
\endgroup
\vss}
\adviplay{e1b}
\adviplay{e2b}
\adviplay{e3b}
\adviplay{e4b}
\adviplay{e5b}
\adviplay{e6b}
\adviplay{e7b}
\adviplay{e8b}
\adviplay{e10b}
\adviplay{e12b}
\adviplay{e14b}
\adviplay{e15b}
\adviplay{e16b}
\adviplay{e18b}
\adviplay{e19b}
\adviplay{e20b}
\adviplay{e22b}
\adviplay{e23b}
\adviwait
\adviplay[slideblue]{e1a}
\adviplay[slideblue]{e2a}
\adviplay[slideblue]{e3a}
\adviplay[slideblue]{e4a}
\adviplay[slideblue]{e5a}
\adviplay[slideblue]{e6a}
\adviplay[slideblue]{e7a}
\adviplay[slideblue]{e8a}
\adviplay[slideblue]{e9a}
\adviplay[slideblue]{e10a}
\adviplay[slideblue]{e11a}
\adviplay[slideblue]{e12a}
\adviplay[slideblue]{e13a}
\adviplay[slideblue]{e14a}
\adviplay[slideblue]{e15a}
\adviplay[slideblue]{e16a}
\adviplay[slideblue]{e17a}
\adviplay[slideblue]{e18a}
\adviplay[slideblue]{e19a}
\adviplay[slideblue]{e20a}
\adviplay[slideblue]{e21a}
\adviplay[slideblue]{e22a}
\adviplay[slideblue]{e23a}
\adviwait
\adviplay[slidegray]{e1a}
\adviplay[slidegray]{e1b}
\adviplay[slidegray]{e2a}
\adviplay[slidegray]{e2b}
\adviplay[slidegray]{e3a}
\adviplay[slidegray]{e3b}
\adviplay[slidegray]{e4a}
\adviplay[slidegray]{e4b}
\adviplay[slidegray]{e5a}
\adviplay[slidegray]{e5b}
\adviplay[slidegray]{e6a}
\adviplay[slidegray]{e6b}
\adviplay[slidegray]{e7a}
\adviplay[slidegray]{e7b}
\adviplay[slidegray]{e8a}
\adviplay[slidegray]{e8b}
\adviplay[slidegray]{e9a}
\adviplay[slidegray]{e10a}
\adviplay[slidegray]{e10b}
\adviplay[slidegray]{e11a}
\adviplay[slideblue]{e12a}
\adviplay[slideblue]{e12b}
\adviplay[slidegray]{e13a}
\adviplay[slidered]{e14a}
\adviplay[slidered]{e14b}
\adviplay[slidegreen]{e15a}
\adviplay[slidegreen]{e15b}
\adviplay[slidegreen]{e16a}
\adviplay[slidegreen]{e16b}
\adviplay[slidegray]{e17a}
\adviplay[slidered]{e18a}
\adviplay[slidered]{e18b}
\adviplay[slidegreen]{e19a}
\adviplay[slidegreen]{e19b}
\adviplay[slidegreen]{e20a}
\adviplay[slidegreen]{e20b}
\adviplay[slidegray]{e21a}
\adviplay[slidered]{e22a}
\adviplay[slidered]{e22b}
\adviplay[slidegreen]{e23a}
\adviplay[slidegreen]{e23b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar sample\hfill\blue{\footnotesize\texttt{arytm\char`\_1.miz}}}
\vbox to 0pt{
\vspace{-1.1em}
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\scriptsize
\gray{\advirecord{f1a}{C} \advirecord{f1b}{:: Non negative real numbers. Part II}
\advirecord{f2a}{C} \advirecord{f2b}{::  by Andrzej Trybulec}
\advirecord{f3a}{C} \advirecord{f3b}{::}
\advirecord{f4a}{C} \advirecord{f4b}{:: Received March 7, 1998}
\advirecord{f5a}{C} \advirecord{f5b}{:: Copyright (c) 1998 Association of Mizar Users}
\advirecord{f6a}{B}}
\advirecord{f7a}{S} \advirecord{f7b}{environ}
\gray{\advirecord{f8a}{B}}
\advirecord{f9a}{S} \advirecord{f9b}{ vocabularies ARYTM_2, BOOLE, ORDINAL2, ARYTM_3, ARYTM_1;}
\advirecord{f10a}{S} \advirecord{f10b}{ notations TARSKI, SUBSET_1, ARYTM_3, ARYTM_2;}
\advirecord{f11a}{S} \advirecord{f11b}{ constructors ARYTM_2;}
\advirecord{f12a}{S} \advirecord{f12b}{ requirements SUBSET;}
\advirecord{f13a}{S} \advirecord{f13b}{ theorems ARYTM_2;}
\gray{\advirecord{f14a}{B}}
\advirecord{f15a}{S} \advirecord{f15b}{begin}
\gray{\advirecord{f16a}{B}}
\blue{\advirecord{f17a}{L} \advirecord{f17b}{reserve x,y,z for Element of REAL+;}}
\gray{\advirecord{f18a}{B}}
\red{\advirecord{f19a}{T} \advirecord{f19b}{theorem Th1:}
\advirecord{f20a}{T} \advirecord{f20b}{  x + y = y implies x = \{\}}}
\green{\advirecord{f21a}{P} \advirecord{f21b}{proof reconsider o = \{\} as Element of REAL+ by ARYTM_2:21;}
\advirecord{f22a}{P} \advirecord{f22b}{  assume x + y = y;}
\advirecord{f23a}{P} \advirecord{f23b}{  then x + y = y + o by ARYTM_2:def 8;}}
\end{alltt}
\endgroup
\vss}
\adviplay{f1b}
\adviplay{f2b}
\adviplay{f3b}
\adviplay{f4b}
\adviplay{f5b}
\adviplay{f7b}
\adviplay{f9b}
\adviplay{f10b}
\adviplay{f11b}
\adviplay{f12b}
\adviplay{f13b}
\adviplay{f15b}
\adviplay{f17b}
\adviplay{f19b}
\adviplay{f20b}
\adviplay{f21b}
\adviplay{f22b}
\adviplay{f23b}
\adviwait
\adviplay[slideblue]{f1a}
\adviplay[slideblue]{f2a}
\adviplay[slideblue]{f3a}
\adviplay[slideblue]{f4a}
\adviplay[slideblue]{f5a}
\adviplay[slideblue]{f6a}
\adviplay[slideblue]{f7a}
\adviplay[slideblue]{f8a}
\adviplay[slideblue]{f9a}
\adviplay[slideblue]{f10a}
\adviplay[slideblue]{f11a}
\adviplay[slideblue]{f12a}
\adviplay[slideblue]{f13a}
\adviplay[slideblue]{f14a}
\adviplay[slideblue]{f15a}
\adviplay[slideblue]{f16a}
\adviplay[slideblue]{f17a}
\adviplay[slideblue]{f18a}
\adviplay[slideblue]{f19a}
\adviplay[slideblue]{f20a}
\adviplay[slideblue]{f21a}
\adviplay[slideblue]{f22a}
\adviplay[slideblue]{f23a}
\adviwait
\adviplay[slidegray]{f1a}
\adviplay[slidegray]{f1b}
\adviplay[slidegray]{f2a}
\adviplay[slidegray]{f2b}
\adviplay[slidegray]{f3a}
\adviplay[slidegray]{f3b}
\adviplay[slidegray]{f4a}
\adviplay[slidegray]{f4b}
\adviplay[slidegray]{f5a}
\adviplay[slidegray]{f5b}
\adviplay[slidegray]{f6a}
\adviplay{f7a}
\adviplay[slidegray]{f8a}
\adviplay{f9a}
\adviplay{f10a}
\adviplay{f11a}
\adviplay{f12a}
\adviplay{f13a}
\adviplay[slidegray]{f14a}
\adviplay{f15a}
\adviplay[slidegray]{f16a}
\adviplay[slideblue]{f17a}
\adviplay[slideblue]{f17b}
\adviplay[slidegray]{f18a}
\adviplay[slidered]{f19a}
\adviplay[slidered]{f19b}
\adviplay[slidered]{f20a}
\adviplay[slidered]{f20b}
\adviplay[slidegreen]{f21a}
\adviplay[slidegreen]{f21b}
\adviplay[slidegreen]{f22a}
\adviplay[slidegreen]{f22b}
\adviplay[slidegreen]{f23a}
\adviplay[slidegreen]{f23b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{11 kinds of lines}
\begin{center}
\begin{tabular}{ll}
\gray{B} & \gray{blank lines} \\
\noalign{\vspace{-\smallskipamount}}
\gray{C} & \gray{comments} \\
\noalign{\vspace{-\smallskipamount}}
\gray{E} & \gray{documentation} \\
\noalign{\vspace{\smallskipamount}}
S & modules: imports and sectioning \\
\noalign{\vspace{\smallskipamount}}
\blue{L} & \blue{contexts} \\
\noalign{\vspace{-\smallskipamount}}
\blue{D} & \blue{definitions} \\
\noalign{\vspace{-\smallskipamount}}
\blue{N} & \blue{notation} \\
\noalign{\vspace{\smallskipamount}}
H & automation: directives \\
\noalign{\vspace{-\smallskipamount}}
X & automation: program code \\
\noalign{\vspace{\smallskipamount}}
\red{T} & \red{theorem statements} \\
\noalign{\vspace{-\smallskipamount}}
\green{P} & \green{proofs}
\end{tabular}\hspace{8em}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{relative sizes: {\small HOL} Light}
\begin{center}
\vbox to 0pt{
\includegraphics[height=18em]{/home/freek/talks/stats/hol_light.eps}\hspace{8em}\strut
\vss}
\end{center}
\vspace{13.5em}
\adviwait

\strut\hfill{almost no module lines} \\
\adviwait
\strut\hfill\red{small definitions part\exclspace!}

\vfill
\end{slide}

\begin{slide}
\slidetitle{relative sizes: Isabelle}
\begin{center}
\vbox to 0pt{
\hspace{-8em}\includegraphics[height=18em]{/home/freek/talks/stats/isabelle.eps}
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{relative sizes: Coq}
\begin{center}
\vbox to 0pt{
\includegraphics[height=18em]{/home/freek/talks/stats/coq.eps}\hspace{8em}\strut
\vss}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{relative sizes: Mizar}
\begin{center}
\vbox to 0pt{
\includegraphics[height=18em]{/home/freek/talks/stats/mizar.eps}\hspace{8em}\strut
\vss}
\end{center}
\vspace{11.9em}
\adviwait

\strut\hfill{no automation lines} \\
\adviwait
\strut\hfill{almost no comments} \\
\adviwait
\strut\hfill\red{large proofs part\exclspace!}

\vfill
\end{slide}

\begin{slide}
\slidetitle{lessons learned}

\begin{itemize}
\item[$\bullet$]
formalizations all are very similar
\smallskip
\adviwait

\gray{{\dots}$\;$despite fundamental differences between proof assistants} \\
\gray{(foundations, interaction styles)}
\medskip
\adviwait

\item[$\bullet$]
formalizations consist primarily of proofs
\bigskip
\adviwait

\item[$\bullet$]
\green{classification of line types in formalizations}
\bigskip
\adviwait

\item[$\bullet$]
\red{small definitions} are good\exclspace!
\adviwait

\item[$\bullet$]
\red{proof automation} is important\exclspace!

\end{itemize}

\vfill
\end{slide}

\end{document}