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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\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}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\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{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large when will it happen?}

Freek Wiedijk \\
University of Nijmegen

Automath Digital Archive Opening Symposium \\
University of Eindhoven \\
2004 05 26, 15:10
\end{slide}

\begin{slide}
\sectiontitle{five heirs to Automath}
\slidetitle{the first heir: \textbf{Agda,} the user experience}
\begin{center}
\red{formalization $=$ lambda term}
\end{center}
\adviwait
\medskip

Swedish system by Thierry \& Catarina Coquand:
\begin{center}
\textbf{Alf} $\;\to\;$ \textbf{Half} $\;\to\;$ \advirecord{a1}{\textbf{C-Half}} $\;\to\;$ \textbf{Alfa} / \blue{\textbf{Agda}}
\adviplay{a1}
\end{center}
\adviwait
\bigskip

\adviplay[slidegreen]{a1}
serious mathematics: \green{\textbf{C-Half}} by Dan Synek
\medskip

formalization of the \green{Hahn-Banach theorem} by Jan Cederquist \\
%\adviwait
%point-free topology \\
constructive mathematics \\
\adviwait
\red{`almost, but not quite, entirely unlike mathematics'}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the second heir: \textbf{Twelf,} the logical framework}
\begin{center}
\red{Automath $\;\approx\;$ $\lambda {\sf P}$ $=$ \textbf{LF}}
\end{center}
\adviwait
\medskip

\blue{Automath restaurant}
\begin{center}
\green{vegetarian food is for a restaurant what \\ constructive mathematics is for a proof checker}
\end{center}
%\adviwait
\medskip

\blue{`logical framework'} \\
three very different logical frameworks:
\red{\textbf{LF}}, Isabelle, Metamath
\adviwait
\medskip

% \blue{\textbf{Twelf}} \\
implementation of \red{\textbf{LF}} by Frank Pfenning and Carsten Sch\"urmann \\
%\adviwait
used for computer science,
not really used for mathematics
\vfill
\end{slide}

\begin{slide}
\slidetitle{the third heir: \textbf{Metamath,} the system}
\begin{center}
\red{fully transparent \& lightning fast}
\end{center}
\adviwait
\medskip

\red{everything} is defined in the formalization \quad \green{(even alpha conversion!)} %\\
%extremely simple framework, traces everything to the axioms
\adviwait
\adviembed{galeon -f file:///usr/local/src/mpegif/nthruc.html}
\adviwait[2]
\bigskip

private system of Norman Megill %\quad (but: \blue{Ghilbert} by Raph Levien)
%\adviwait

implemented in C: checks its whole library \red{in a few seconds} \\
\dashskip \blue{$\to$ like the Automath implementation by FW}
\adviwait
\bigskip

various logics: \textbf{ZFC} set theory, quantum logic
\adviwait
%\medskip

library of mathematics from \textbf{ZFC} up to the complex numbers \\
\dashskip \blue{$\to$ like Landau's Grundlagen der Analysis}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the fourth heir: \textbf{Mizar,} the goal}
\begin{center}
\red{let's do real mathematics!}
\end{center}
\adviwait
\medskip

biggest library of formalized mathematics in the world
\green{
\begin{itemize}
\item[] 46,000 lemmas
\item[] 1.7 million lines
\item[] 60 megabytes
\end{itemize}
}
\adviwait
\medskip

Polish system by Andrzej Trybulec \\
based on \textbf{ZFC} set theory
\adviwait

%source not freely available, no small kernel
%\adviwait
\medskip

really looks like mathematics: \red{mathematical mode} \\
\dashskip \blue{$\to$ formal proof sketches}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the fifth heir: \textbf{HOL Light,} the de Bruijn criterion}
\begin{center}
\red{the best proof checker of the world}
\end{center}
\adviwait
collection of formalizations of irrationality of $\sqrt{2}$ in sixteen systems \\
\green{\textbf{Mizar} and \textbf{HOL Light:} shortest formalizations \& came in first}
\adviwait
\bigskip

private reimplementation of HOL by John Harrison \\
\red{very small kernel}: %\red{de Bruijn criterion} \\
nine pages of ML including comments
\adviwait
\medskip

\red{strong automation}: LCF approach
\adviwait
\medskip

\red{serious library of mathematics} \\
one of the three formalizations of the \green{Fundamental Theorem of Algebra} \\
system selected for \blue{\textbf{Flyspeck}}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{it {will} happen}
\slidetitle{let's formalize mathematics!}
\begin{center}
\green{
Automath \\
Mizar \\
QED manifesto \\
MBase \\
C-CoRN \\
\dots
}
\end{center}
\adviwait

until now it just remains promises for the future
\adviwait
\smallskip

real mathematicians are not yet interested \\
\green{(and we ourselves don't formalize our proofs either!)}
\smallskip

\begin{center}
\red{why doesn't it take off?} \\
\red{what's missing?}
\end{center}
\vspace{-16pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{why are mathematicians not interested?}
\slidetitle{it just takes much too long \dots \hfill (the cost is too high)}
$$\adviwait\mbox{de Bruijn factor} = {\mbox{size of formalization} \over \mbox{size of normal text}}$$
\green{question: is this a constant?}
\begin{center}
\green{experimental:} around \textbf{4}
\end{center}
\adviwait
\bigskip
$$\mbox{de Bruijn factor in time} = {\mbox{time to formalize} \over \mbox{time to understand}}$$
\begin{center}
\medskip
much larger than \textbf{4}
\end{center}
\medskip
\begin{center}
\red{formalizing one textbook page $\;\approx\;$ 1 man$\cdot$week $=$ 40 man$\cdot$hours}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} and what's the use? \hfill (the benefit is too low)}
\begin{center}
\adviwait
\red{l'art pour l'art}
\end{center}
\medskip
Paul Libbrecht in Saarbr\"ucken: `mental masturbation'
\adviwait
\medskip

it's not \textbf{impossibly} expensive \\
formalizing \green{all of undergraduate mathematics} $\approx$ 140 man$\cdot$years \\
% no small group can do this on their own! \\
the price of about \textbf{one} Hollywood movie
\adviwait
\medskip

but: after formalization one just has a big incomprehensible file \\
\red{we don't have a good argument yet for spending that money}
%\adviwait
\medskip
\begin{center}
\textbf{certainty that it's fully correct?}
\end{center}
\green{is that important enough to pay for 140 man$\cdot$years?}
\vfill
\end{slide}

\begin{slide}
\slidetitle{it doesn't resemble mathematics! \hfill (not my business)}
\adviwait
most systems: \blue{proof} = list of tactics = \red{unreadable computer code} \\
%\adviwait
\green{even in `mathematical mode' systems}: \red{still looks like code}
\adviwait
\medskip

\blue{even formulas:} \red{too much `decoding' needed to understand what it says}

\medskip
\begin{alltt}\footnotesize
  Variable J : interval.     Hypothesis pJ : proper J.
  Variable F, G : PartIR.    Hypothesis derG : Derivative J pJ G F.
  Let G_inc := Derivative_imp_inc _ _ _ _ derG.\medskip
  Theorem Barrow : forall a b (H : Continuous_I (Min_leEq_Max a b) F) Ha Hb,\toolong
   let Ha' := G_inc a Ha in let Hb' := G_inc b Hb in
   Integral H [=] G b Hb'[-]G a Ha'.
\end{alltt}
\adviwait
\smallskip
$$\green{G' = F \;\Rightarrow\; \int_a^b F(x)\,dx = G(b) - G(a)}$$
\adviwait
\vspace{-\medskipamount}
\vspace{-\smallskipamount}

another barrier:
%\adviwait
\red{you won't sell intuitionism to classical mathematicians}\toolong
\vspace{-10pt}
\vfill
\end{slide}

%and what doesn't help either:
%- "we will build the system, let someone else do the formalizations"
%- one system among many
%- the focus on computer science

\begin{slide}
\sectiontitle{so what is needed most?}
\slidetitle{automation}
\begin{itemize}
\item[$\bullet$] proof search: not very powerful, not very important
\item[$\bullet$] \red{decision procedures}: very important, main strength of PVS
\adviwait
\smallskip

\blue{computer algebra} \\
\green{macsyma, maple, mathematica} \quad (really: \blue{computer calculus})
\adviwait
\medskip

\red{high school mathematics should be trivial!}
\end{itemize}
\begin{eqnarray*}
x=i/n\;,\!\!\quad n=m+1 &\red{\vdash}& n!\cdot x=i\cdot m! \\
\noalign{\smallskip}
{k\over n}\ge 0 &\red{\vdash}& \left|{n-k\over n}-1\right|={k\over n} \\
n\ge 2\;,\!\!\quad x={1\over n+1} &\red{\vdash}& {x\over 1-x}<1 \\
\noalign{\vspace{-3em}}
\end{eqnarray*}
\vfill
\end{slide}

\end{document}