\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}
\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}
\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}
\slidetitle{\Large how to build a library of formalized \white{\advirecord{a1}{\rlap{mathematics}}}\adviplay{a1}\advirecord{a2}{\textbf{mathematics}}}

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

\red{MathWiki Workshop} \\
University of Edinburgh
\smallskip

{2007\hspace{3pt}10\hspace{3pt}31, 11\hspace{1pt}:\hspace{1.8pt}00}

\adviwait
\adviplay[white]{a1}
\adviplay[slideblue]{a2}

\end{slide}

\begin{slide}
\sectiontitle{state of the art}
\slidetitle{top 100}
\begin{center}
\green{\texttt{http://www.cs.ru.nl/\char`\~freek/100/}}
\end{center}
\begin{center}
\strut{google\hspace{3pt} }\gray{\fbox{\texttt{\hspace{2pt}\strut \red{100 theorems}\hspace{3pt}}}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{current systems}
\begin{itemize}
\item[\blue{$\bullet$}]
\blue{{interesting}}

\begin{itemize}
\item[]
{{HOLs}}
\begin{itemize}
\item[--]
\red{HOL Light} \hfill\green{63}\hspace{15em}

\item[--]
\red{Proof\hspace{.5pt}Power} \hfill\green{39}\hspace{15em}

\item[--]
\red{Isabelle/HOL} \hfill\green{36}\hspace{15em}

\end{itemize}

{{non-HOLs}}

\begin{itemize}
\item[--]
\red{{Coq}} \hfill\green{39}\hspace{15em}

\item[--]
\red{{Mizar}} \hfill\green{39}\hspace{15em}

\end{itemize}
\end{itemize}
\adviwait

\item[\gray{$\bullet$}]
\gray{not in the top five}
\begin{itemize}
\item[]
\begin{itemize}
\item[--]
\gray{{PVS}} \hfill\gray{15}\hspace{15em}

\item[--]
\gray{{NuPRL}} \hfill\gray{12}\hspace{15em}

\item[--]
\gray{{ACL2}} \hfill\gray{8}\hspace{15em}

\end{itemize}
\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the 20 unformalized theorems}

\footnotesize
\strut\hspace{-.75em}\begin{tabular}{l}
12. The Independence of the Parallel Postulate \\
16. Insolvability of General Higher Degree Equations \\
21. \textsl{\green{Green's Theorem}} \\
24. \textsl{\green{The Undecidability of the Continuum Hypothesis}} \\
28. Pascal's Hexagon Theorem \\
29. Feuerbach's Theorem \\
33. \textsl{\red{\advirecord{b}{Fermat's Last Theorem}}\adviplay[slidegreen]{b}} \\
41. Puiseux's Theorem \\
43. \textsl{\green{The Isoperimetric Theorem}} \\
47. The Central Limit Theorem \\
48. \textsl{\green{Dirichlet's Theorem}} \\
50. The Number of Platonic Solids \\
53. Pi is Trancendental \\
56. The Hermite-Lindemann Transcendence Theorem
\end{tabular}\hspace{-3em}%
\begin{tabular}{l}
\ \\
\ \\
\ \\
\ \\
\ \\
59. The Laws of Large Numbers \\
62. Fair Games Theorem \\
67. e is Transcendental \\
76. Fourier Series \\
82. Dissection of Cubes \\
92. Pick's Theorem \\
\ \\
\ %
\end{tabular}$\hspace{-3em}$\strut
\adviwait
\adviplay[slidered]{b}

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

\begin{slide}
\slidetitle{current libraries}
\begin{itemize}
\item[$\bullet$]
\red{many people}, badly organized
\smallskip

\begin{itemize}
\item[--]
\textbf{MML} \hfill\green{\rlap{Mizar}}\hspace{10em}\strut

\item[--]
\textbf{AFP} \hfill\green{\rlap{Isabelle/HOL}}\hspace{10em}\strut

\item[--]
\textbf{Coq contribs} \hfill\green{\rlap{Coq}}\hspace{10em}\strut

\end{itemize}
\medskip

\item[$\bullet$]
one person, \red{well organized}
\smallskip

\begin{itemize}
\item[--]
\textbf{John Harrison} \hfill\green{\rlap{HOL Light}}\hspace{10em}\strut
%\adviwait

\item[--]
\textbf{Georges Gonthier} \hfill\green{\rlap{Coq}}\hspace{10em}\strut

\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{looks do matter}
\slidetitle{fake problems}
\begin{itemize}
\item[$\bullet$]
\textbf{`it is too much work'}
\adviwait

\textsl{de Bruijn factor in space:} \green{about 4 times} \\
\textsl{de Bruijn factor in time:} about 10 times = \green{about 1 week/page} \\
\adviwait
\textsl{all of undergraduate mathematics:} \green{about 140 man-years} \\
\adviwait
\strut\hfill \red{not expensive!}
\adviwait

\item[$\bullet$]
\textbf{`it is not useful'}
\adviwait

-- correctness \\
-- {explicitness} \\
\adviwait
-- \red{art}
\smallskip
\adviwait

\item[$\bullet$]
\textbf{{`mathematicians will not want it'}}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{real problems}
\begin{itemize}
\item[$\bullet$]
\green{insufficient automation}

\begin{itemize}
\item[--]
computer algebra is much more powerful
\adviwait

\item[--]
automation of \red{high school mathematics}
\begin{eqnarray*}
x=i/n\;,\;\; n=m+1 &{\vdash}& n!\cdot x=i\cdot m! \\
\noalign{\smallskip}
{k\over n}\ge 0 &{\vdash}& \left|{n-k\over n}-1\right|={k\over n} \\
n\ge 2\;,\;\; x={1\over n+1} &{\vdash}& {x\over 1-x}<1
\end{eqnarray*}

\end{itemize}
\medskip
\adviwait

\item[$\bullet$]
\green{no good way to write {calculus}}

\begin{center}
formulas in proof assistants $\;\leftrightarrow\;$ \red{formulas in a calculus textbook}
\end{center}

\end{itemize}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 1}
\vfill
\red{a library that does not code the calculus formula
$$ \sum_{n = -\infty}^\infty e^{int} {1 \over 2\pi} \int_{-\pi}^\pi e^{-ins} f(s)\, ds $$
in a way that is very close to the computer algebra term
\begin{center}
\texttt{sum(e\char`\^(I*n*t)/(2*pi)*int(e\char`\^(-I*n*s)*f(s),s=-pi..pi),} \\
\texttt{n=-infinity..infinity)}
\end{center}
will never be widely used}
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\slidetitle{real problems (continued): {too unlike real mathematics}}
\begin{itemize}
\item[$\bullet$]
\green{the look of the proofs}
\smallskip
\begin{alltt}\footnotesize
\gray{intros k l H; induction H as [|l H].
intros; absurd (S k <= k); auto with arith.
destruct H; auto with arith.}
\end{alltt}
\medskip
\adviwait

\item[$\bullet$]
\green{constructive mathematics}
\smallskip

\begin{itemize}
\item[--]
reasoning by cases

\gray{\textsl{a quadratic equation will have zero, one, or two roots, depending on the sign of the discriminant}}
\adviwait
\smallskip

\item[--]
extensionality

\gray{\textsl{what do you mean: `the complex square root is not extensional?'}}

\end{itemize}
\end{itemize}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 2}
\vfill
\strut \red{a library that supports constructive reasoning will never be widely used \\
\adviwait
\strut {\dots} unless the constructivity can be completely ignored by classical users \\
\adviwait
\strut {\dots} but that will not be feasible }
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\slidetitle{portability to the future}
idiosyncratic $\;\leftrightarrow\;$ \red{\advirecord{c2}{canonical}}\adviplay{c2}
\medskip
\adviwait
\adviplay[slidered]{c2}
\adviwait

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

\begin{itemize}
\item[]
\gray{\advirecord{c1}{HOL}}\adviplay[slidered]{c1}
\adviwait
\adviplay[slidegray]{c1}

\item[]
\red{FOL} \adviwait \gray{+ soft types}
\end{itemize}
\medskip
\adviwait

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

\begin{itemize}
\item[]
\red{declarative proofs}

\begin{itemize}
\item[--]
Mizar, Isar, Christophe Raffalli, Pierre Corbineau, \dots

\item[--]
Fitch-style natural deduction

\end{itemize}
\medskip

\green{independent of the specifics of the system}
\end{itemize}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{portability to the future (continued)}

{\Large $${1\over 0}\;?\medskip$$}

\strut\hfill\adviwait
${1\over 0} = \red{0}$?\hfill\adviwait
$1\over 0$ is an unknown number?\hfill\adviwait
$1\over 0$ is a non-denoting term?\hfill
\advirecord{d3}{$1\over 0$ is \red{illegal}?}\hfill
\strut

\vfill
\small
\green{\strut\hfill\advirecord{d1}{(I do not like proof terms in my formulas either)} \\
\strut\hfill\advirecord{d2}{(I like partial logics about as much as I like constructive logics)}}%
\adviwait
\adviplay[slidegreen]{d2}%
\adviwait
\adviplay{d3}%
\adviwait
\adviplay[slidegreen]{d1}%

\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 3}
\vfill
\strut \red{none of the existing systems is portable to the future \\
\adviwait
\strut {\dots} so any library of formal mathematics will have to be redone later}
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\sectiontitle{it's a social problem}
\slidetitle{definitions}
\adviwait
\white{\advirecord{e3}{three}}\adviplay{e3}\advirecord{e2}{\llap{four}} kinds of information in a formal library
\begin{itemize}
\item[--]
definitions
\item[--]
\red{\advirecord{e1}{statements}}\adviplay{e1}
\item[--]
proofs
\adviwait
\adviplay[white]{e3}\adviplay{e2}
\item[\gray{--}]
\gray{tactics / decision procedures}
\end{itemize}
\bigskip
\adviwait
\adviplay[slidered]{e1}

the $\,$\red{statements}$\,$ should be what matters
\adviwait
\bigskip

the right definitions? \\
the right \textbf{notions}\hspace{.5pt}

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

\begin{slide}
\slidetitle{are conceptual advances helpful?}

\begingroup
\footnotesize
\adviwait
coercions \adviwait\\
subtyping \adviwait\\
record types \adviwait\\
module systems \adviwait\\
type universes \adviwait\\
canonical structures \adviwait\\
binders \adviwait\\
induction-recursion \adviwait\\
coinduction \adviwait\\
\green{partiality} \adviwait
\endgroup
\medskip

\strut\hfill\hfill\red{all pretty much irrelevant}\hfill\strut

\vfill
\end{slide}

\begin{slide}
\slidetitle{why don't we have a good library of formalized mathematics yet?}
what are the main obstacles?
\adviwait
\begin{itemize}
\item[$\bullet$]
social?
%\adviwait
\item[$\bullet$]
engineering?
%\adviwait
\item[$\bullet$]
mathematical?
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{obstacles}
\begin{itemize}
\item[$\bullet$]
\textbf{social problem}

\red{many people \textsl{and} well organized}

how to decide on the definitions? \\ % + notations? \\
how to decide on the \green{names of the theorems}? \\
how to decide on the structure of the library?

\item[$\bullet$]
\textbf{engineering problem}

good formalization of calculus \\
automation of \green{high school mathematics}

\item[$\bullet$]
\textbf{mathematical problem}

how to deal with \green{partiality}?

\end{itemize}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 4}
\vfill
\strut \red{building a good library of formal mathematics is a social problem \adviwait\\
\strut {\dots} the main problem is to keep the library well organized \adviwait\\
\strut {\dots} {\footnotesize after having solved the problem of getting participants in the first place}}
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\slidetitle{looking for a solution: the internet}

\textbf{{`benevolent dictatorship'}}
\bigskip

\blue{examples}

\begin{itemize}
\item[--]
Linux
\item[--]
Wikipedia
\end{itemize}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 5}
\vfill
\strut \red{a formal library should be \textbf{flat} \\%\adviwait\\
\strut {\dots} consisting of a sequence of `articles' \\%\adviwait\\
\strut {\dots} consisting of a sequence of `lemmas'}
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\slidetitle{looking for a solution: traditional mathematics}

\textbf{`many different variations that still are usable together'}
\bigskip
\adviwait

Coq and Isabelle contribs are \red{not} like this (\textsl{not} used together) \\
\adviwait
John's and Georges' libraries are \red{not} like this (just \textsl{one} variation) \\
\adviwait
{Mizar's MML \textsl{is} \red{very much} like this}
\adviwait
\bigskip
\bigskip

%\red{but:}
\blue{however} `articles' should have \textsl{two parts}: $\,$\green{preliminaries / content}
\adviwait

\begin{itemize}
\item[--]
each article \blue{owned by someone}
\item[--]
\textsl{preliminaries} \blue{point} to the articles where the lemmas should go
\item[--]
\textsl{content} part should stay together
\end{itemize}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 6}
\vfill
\strut \red{a formal library should not just be a `sea of lemmas' \adviwait\\
\strut {\dots} because a proof assistant is not a stateless thing} \\
\strut
\vfill
\end{slide}
\slidepagestyle{fw}

\addtocounter{slide}{-1}
\slidepagestyle{fw0}
\begin{slide}
\xslidetitle{provocative statement 7}
\vfill
\strut \red{linking existing proof assistants together is not useful \adviwait\\
\strut {\dots} for the same reasons that these systems are not portable to the future\toolong} \\
\strut
\vfill
\end{slide}
\slidepagestyle{fw}

\begin{slide}
\slidetitle{the aim}
\bigskip
\begin{center}
{formalization for \textbf{communication} of mathematics}%\hspace{.5pt}!}
\end{center}
\adviwait
\bigskip
\bigskip
\begin{center}
proof assistants that are \textbf{visual}?
\end{center}

\vfill
\end{slide}

\end{document}