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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.55,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}{#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}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large John Harrison's formalization of the \smallskip\\ AKS primality test\smallskip}

Freek Wiedijk \\
University of Nijmegen

Intercity Number Theory Seminar \\
Nijmegen

2003 06 06, 16:00
\end{slide}


\begin{slide}
\sectiontitle{AKS}
\slidetitle{mathematics as we know it}
from \green{proving primality after Agrawal-Kayal-Saxena} by
Daniel Bernstein:
\medskip

\rightskip=0pt
\baselineskip=16pt
\lineskip=0pt
\textbf{Theorem 2.3} $\,$(2002.08.14; Manindra Agrawal, Neeraj Kayal, Nitin Saxena, and Hendrik W. Lenstra, Jr.)\textbf{.}
\textsl{Let $n$, $r$, and $v$ be positive integers.
Let $S$ be a finite set of integers.
Assume that $n$ and $r$ are coprime;
that $n$ has order $v$ modulo $r$;
that ${\sf gcd}\,\{n,b - b'\} = 1$ for all distinct $b, b'\in S$;
that $\big({\#S + \phi(r) - 1\atop\#S}\big)\ge n^{2d\lfloor\sqrt{\phi(r)/d}\rfloor}$ for every positive integer $d$ dividing $\phi(r)/v$;
and that $(x + b)^n = x^n + b$ in the ring $({\bf Z}/n)[x]/(x^r - 1)$ for all $b\in S$.
Then $n$ is a power of a prime.}
%\adviwait
\smallskip

\red{key theorem of $\,\mbox{\small PRIMES}\in\mbox{P}$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{moving the theorem into the computer}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\begingroup
\small
\begin{verbatim}
!n r v s.
  ~(r = 1) /\
  FINITE s /\
  coprime(n,r) /\
  (order(r) n = v) /\
  (!b b'. b IN s /\ b' IN s /\ ~(b' = b)
          ==> (gcd(n,dist(b,b')) = 1)) /\
  (!d. d divides (phi(r) DIV v)
       ==> binom(CARD s + phi(r) - 1,CARD s)
           >= n EXP (2 * d * ISQRT(phi(r) DIV d))) /\
  (!b. b IN s
       ==> ((X + %b)^n === X^n + %b) (modulo {(%n),(X^r - %1)}))
  ==> ?p k. prime p /\ (n = p EXP k)
\end{verbatim}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{the context}
\red{John Harrison}

got his PhD in Cambridge on automated theorem proving \\
works at Intel proving Pentium chips correct \\
formalizes mathematics for fun in his spare time
\adviwait
\medskip

\red{HOL Light} \\
\green{HOL = Higher Order Logic}

John Harrison's re-implementation of the HOL proof assistant \\
implemented in the ML programming language

%`system' = ML interpreter + over a thousand ML functions loaded \\
%HOL formalization = ML program
%\adviwait
%\medskip
%
%\red{AKS formalization}

\vfill
\end{slide}

\begin{slide}
\slidetitle{AKS formalization}
\begin{itemize}
\item[$\bullet$]
weak prime number theorem \blue{(done)}
$$\mbox{\llap{$n\ge 3 \;\;\Rightarrow\;\;$}}\, {1\over 2} {n\over\ln n}\le\pi(n)\le 5 {n\over\ln n}$$
\item[$\bullet$]
theory of cyclotomic polynomials \blue{(done)}
\item[$\bullet$]
\red{theorem 2.3 from Daniel Bernstein's paper} \blue{(work in progress)}
\item[$\bullet$]
primality prover based on AKS \blue{(future)}
\item[$\bullet$]
complexity analysis of the AKS algorithm \blue{(future)}
\end{itemize}
\adviwait
\medskip

\green{all proofs are fully formal all the way down to the axioms}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{HOL Light}
\slidetitle{the axioms}
\textbf{types}

\strut\rlap{base types}$\hspace{10em}$ \textbf{bool} \green{= $\{\top,\bot\}$}\quad\textbf{ind} \green{= some infinite set} \\
\rlap{function types}$\hspace{10em}$ $A\to B$ \\
\rlap{non-empty subtypes}$\hspace{10em}$ $A'$ \\
\strut$\hspace{10em}$ \green{type $A$ + predicate in $A\to\mbox{bool}$}
\adviwait

\textbf{objects}

\strut\rlap{equality}$\hspace{10em}$ \rlap{$=_A$}$\hspace{4em}$\green{$\in A\to A\to\mbox{bool}$} \\
\rlap{choice operator}$\hspace{10em}$ \rlap{$\mbox{@}_A$}$\hspace{4em}$\green{$\in (A\to\mbox{bool})\to A$} \\
\rlap{subtype mappings}$\hspace{10em}$ $\hspace{4em}$\green{$\in A'\to A$\quad $\in A\to A'$} \bigskip\\
\adviwait
\rlap{\red{$\lambda$-terms}}$\hspace{10em}$ \rlap{$\lambda x.\,F[x]$}$\hspace{4em}$\green{$\in A\to B$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{logic}
\textbf{examples of HOL objects}

\begin{tabular}{clcl}
$\top\!\!$ & \green{$\in\mbox{bool}$} & $\equiv$ & $(\lambda x.\,x) =_{{\sf bool}\to {\sf bool}} (\lambda x.\,x)$ \\
$\forall_A\!\!$ & \green{$\in (A\to\mbox{bool})\to\mbox{bool}$} & $\equiv$ & $\lambda P.\, (P =_{A\to {\sf bool}} (\lambda x.\,\top))$
\end{tabular}
\adviwait
\medskip

\red{no distinction between terms and statements, just $\lambda$-terms}
$$\forall x\in A.\,P[x] \quad\mbox{is represented by}\quad \forall_A \, (\lambda x.\,P[x])\smallskip$$
\begin{tabular}{rcl}
term &=& term \\
statement &=& term denoting an object in type bool \\
theorem &=& term denoting the object $\top$ in type bool
\end{tabular}
\adviwait
\medskip

\red{HOL logic is weaker than ZFC set theory (but not much)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{ML}
\red{`functional programming'}

a more mathematical way of programming \\
\green{Lisp, ML, Haskell}
\adviwait
\medskip

ML originally spin-off of the LCF proof assistant (predecessor of HOL) %\\
%ML = `meta-language'
\adviwait
\medskip

\textbf{example}\quad \advirecord{funpow}{$f^n(x)$}

\begin{flushleft}
\verb|#|\adviwait\red{\texttt{let rec funpow n f x =}}\\
\verb|  |\red{\texttt{if n < 1 then x else funpow (n-1) f (f x);;}}\\
\adviplay[slidegreen]{funpow}
\adviwait
\verb|funpow : int -> ('a -> 'a) -> 'a -> 'a = <fun>|\\
\verb|#|\adviwait\red{\texttt{funpow 6 (fun n -> 3*n-1) 1;;}}\\
\adviwait
\verb|- : int = 365|\\
\verb|#|
\end{flushleft}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why should we trust a proof assistant?}
%\adviwait
very small `proof kernel'
\medskip

\textbf{de Bruijn criterion} \\
\green{if you can trust the kernel, you can trust the whole system}
\adviwait
\bigskip

\red{HOL Light kernel}

282 lines of ML \\
only 9 pages (with many comments!)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{HOL definitions}
\slidetitle{the shape of a formalization}
HOL files contain
\begin{itemize}
\item[$\bullet$]
\textbf{definitions} (of HOL types, of HOL objects)

\red{minor part of the files: about 2\%}
\adviwait

\item[$\bullet$]
\textbf{theorems} (statements, each with a proof)

\red{major part of the files: about 80\%} \\
\green{long necklace of lemmas} \\
statements are readable formulas, proofs are unreadable `code'
\adviwait

\item[$\bullet$]
\textbf{implementation of tactics}

small programs \\
solve well-defined \& mathematically trivial sub-problems

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of HOL types}

\begin{tabular}{lcl}
\red{\texttt{num}} &$=$& $\mathbb N$ \vspace{-\smallskipamount}\\
\texttt{int} &$=$& $\mathbb Z$ \vspace{-\smallskipamount}\\
\texttt{real} &$=$& $\mathbb R$ \vspace{-\smallskipamount}\\
\texttt{complex} &$=$& $\mathbb C$ \smallskip\\
\adviwait
\texttt{($A$)list} &$=$& finite lists over the type $A$ \vspace{-\smallskipamount}\\
\adviwait
\texttt{(complex)list} &$=$& ${\mathbb C}\;\hspace{.2pt}[X]$ \smallskip\\
\adviwait
$\texttt{int}\to\texttt{int}$ &$=$& functions from $\mathbb Z$ to $\mathbb Z$ \vspace{-\smallskipamount}\\
\red{\texttt{intpoly}} &$=$& ${\mathbb Z}[X]$ \smallskip\\
\adviwait
\red{$\texttt{intpoly}\to\texttt{bool}$} &$=$& the subsets of ${\mathbb Z}[X]$
\end{tabular}
\adviwait
\medskip

%\red{rather `flat' types} \\
\green{no parametrized type for polynomials over an arbitrary ring}
\adviwait

\green{no type distinction between subsets of ${\mathbb Z}[X]$ and ideals of ${\mathbb Z}[X]$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{ways to define a HOL function, variant I: abbreviations}
\begin{flushleft}
\verb|let dist = new_definition| \\
\verb|  `|\red{\texttt{dist}}\verb|(m,n) = (m - n) + (n - m)`;;|
\end{flushleft}
\adviwait

\begin{flushleft}
\verb|let X = new_definition| \\
\verb|  `|\red{\texttt{X}}\verb| = mk_intpoly(\x. x)`;;|
\end{flushleft}
\adviwait

\medskip
\blue{definitions using the Hilbert choice operator \texttt{@} (`epsilon')}
\begin{flushleft}
\verb|let ISQRT = new_definition| \\
\verb|  `|\red{\texttt{ISQRT}}\verb| n = @m. m EXP 2 <= n /\ n < (m + 1) EXP 2`;;|
\end{flushleft}
\adviwait

\begin{flushleft}
\verb|let aprimedivisor = new_definition| \\
\verb|  `|\red{\texttt{aprimedivisor}}\verb| q = @p. prime p /\ p divides q`;;|
\end{flushleft}

%\begin{flushleft}
%\verb|#map type_of [`dist`; `X`; `ISQRT`; `aprimedivisor`];;| \\
%\verb|it : hol_type list =| \\
%\verb| [`:(num#num)->num`; `:intpoly`; `:num->num`; `:num->num`]| \\
%\verb|#|
%\end{flushleft}

\vfill
\end{slide}

\begin{slide}
\slidetitle{ways to define a HOL function, variant II: recursive definitions}
definition with \green{recursion} is built into HOL
%\adviwait
\medskip

\textbf{example}
\begin{flushleft}
\verb|let EXP = |\green{\texttt{new\char`\_recursive\char`\_definition}}\verb| num_RECURSION| \\
\verb| `(!m. m |\red{\texttt{EXP}}\verb| 0 = 1) /\| \\
\verb|  (!m n. m |\red{\texttt{EXP}}\verb| (SUC n) = m * (m |\red{\texttt{EXP}}\verb| n))`;;|
\end{flushleft}
\adviwait
\bigskip

\blue{recursion principle}
\begin{flushleft}
\texttt{num\char`\_RECURSION} \\
\texttt{|- !e f.\ ?fn.\ (fn 0 = e) /\char`\\\ (!n.\ fn (SUC n) = f (fn n) n)}
\end{flushleft}
shows that the recursion is well-founded

\vfill
\end{slide}

\begin{slide}
\slidetitle{ways to define a HOL function, variant III: inductive definitions}
\green{inductive} definitions (\green{`smallest set closed under \dots'}) also built into HOL$\!$
\medskip

\textbf{example}

\blue{`the ideal generated by a set $\texttt{s}\subseteq {\mathbb Z}[X]$'}
\adviwait
\smallskip

\begin{flushleft}
\verb|let idealgen_RULES,idealgen_INDUCT,idealgen_CASES =| \\
\verb|  |\green{\texttt{new\char`\_inductive\char`\_definition}} \\
\verb|  `(!x. s x ==> |\red{\texttt{idealgen}}\verb| s x) /\| \\
\verb|   |\red{\texttt{idealgen}}\verb| s (%0) /\| \\
\verb|   (!a b. idealgen s a /\ idealgen s b| \\
\verb|          ==> |\red{\texttt{idealgen}}\verb| s (a - b)) /\| \\
\verb|   (!a x. idealgen s a ==> |\red{\texttt{idealgen}}\verb| s (a * x))`;;|
\end{flushleft}
\adviwait
\medskip

$\texttt{idealgen} \in \texttt{(intpoly}\to\texttt{bool)}\to\texttt{(intpoly}\to\texttt{bool)}$

\vfill
\end{slide}

\begin{slide}
\slidetitle{syntactic sugar}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\begin{flushleft}\small
\verb|!n r v s.| \\
\verb|  ~(r = 1) /\| \\
\verb|  FINITE s /\| \\
\verb|  coprime(n,r) /\| \\
\verb|  (order(r) n = v) /\| \\
\verb|  (!b b'. b IN s /\ b' IN s /\ ~(b' = b)| \\
\verb|          ==> (gcd(n,dist(b,b')) = 1)) /\| \\
\verb|  (!d. d divides (phi(r) DIV v)| \\
\verb|       ==> binom(CARD s + phi(r) - 1,CARD s)| \\
\verb|           >= n EXP (2 * d * ISQRT(phi(r) DIV d))) /\| \\
\verb|  (!b. b IN s| \\
\verb|       ==> |\advirecord{congruence}{\texttt{((X + \char`\%b)\char`\^n === X\char`\^n + \char`\%b) (modulo \char`\{(\char`\%n),(X\char`\^r - \char`\%1)\char`\})}}\adviplay{congruence}\verb|)| \\
\verb|  ==> ?p k. prime p /\ (n = p EXP k)|
\end{flushleft}
%\adviwait
\adviplay[slidered]{congruence}

\vfill
\end{slide}

\begin{slide}
\slidetitle{`$(X + b)^n = X^n + b\;\mbox{ in the ring }\,({\mathbb Z}/n{\mathbb Z})[X]/(X^r - 1)$'}
\begin{center}
\red{\texttt{((X + \char`\%b)\char`\^n === X\char`\^n + \char`\%b) (modulo \char`\{(\char`\%n),(X\char`\^r - \char`\%1)\char`\})}}
\end{center}
\adviwait
\medskip

\textbf{functions}
\smallskip

\begin{tabular}{ccl}
%\verb|X| &{\small $\in$}$\hspace{-.5em}$& {\small \verb|intpoly|} \\
\red{\texttt{\char`\%}} &{$\in$}$\hspace{-.5em}$& {$\texttt{num}\to\texttt{intpoly}$} \smallskip\\
\adviwait
%\green{\texttt{(}}\verb|===|\green{\texttt{)}} &{\small $\in$}$\hspace{-.5em}$& {\small $\texttt{intpoly}\to\texttt{intpoly}\to\texttt{(intpoly}\to\texttt{bool)}\to\texttt{bool}$}$\hspace{-1.5em}$ \\
\texttt{\red{\char`\{}(\char`\%n)\red{,}(X\char`\^r - \char`\%1)\red{\char`\}}}$\hspace{-.5em}$ &{$\in$}$\hspace{-.5em}$& {$\texttt{intpoly}\to\texttt{bool}$} %\\
%\verb|modulo| &{\small $\in$}$\hspace{-.5em}$& {\small $\texttt{(intpoly}\to\texttt{bool)}\to\texttt{(intpoly}\to\texttt{bool)}$}
\end{tabular}
\adviwait
\bigskip

%\textbf{relevant definitions}
\begin{flushleft}
\verb|let intpolycong = new_definition| \\
\verb|  `(p |\red{\texttt{===}}\verb| q) (j:intpoly->bool) = (p - q) IN j`;;|
\end{flushleft}
\begin{flushleft}
\verb|let modulo = new_definition| \\
\verb|  `|\red{\texttt{modulo}}\verb| = idealgen`;;|
\end{flushleft}
\adviwait
\medskip

\green{\textbf{note:} this talks about polynomials in ${\mathbb Z}[X]$ instead of $({\mathbb Z}/n{\mathbb Z})[X]$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{some AKS statistics}

\medskip
\begin{tabular}{lcccc}
&& \blue{outside AKS} && \blue{inside AKS} \\
HOL type definitions && 17 && 1\advirecord{AKS-type}{\rlap{\enskip $\leftarrow$ \texttt{intpoly}}} \\
HOL function definitions && 308 && 45 \\
theorems + proofs && 2811 && \red{377} \\
ML functions (tactics) && 1222 && 14
\end{tabular}
\bigskip

\green{currently the AKS files are about 1/7$\,$th the size of the basic library}
\adviwait
\adviplay[slidered]{AKS-type}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{zooming in on a (trivial) lemma}
\slidetitle{the 10 HOL files of AKS}

\begin{tabular}{ll}
\texttt{cyclotomic.ml} &  cyclotomic polynomials \vspace{-\smallskipamount}\\
\texttt{isqrt.ml} &  integer square root \vspace{-\smallskipamount}\\
\texttt{intpoly.ml} &  ring of univariate integer polynomials \vspace{-\smallskipamount}\\
\texttt{fermatpoly.ml}$\quad$ &  Fermat's Little Theorem for polynomials \vspace{-\smallskipamount}\\
\texttt{psi.ml} &  analysis of Chebyshev's $\psi$ \vspace{-\smallskipamount}\\
\advirecord{thefilearrow}{\llap{$7\%\to\enskip$}}\advirecord{thefile}{\texttt{theta.ml} & similar analysis of $\theta$}\adviplay{thefile} \vspace{-\smallskipamount}\\
\texttt{bertrand.ml} &  Bertrand conjecture, just for fun \vspace{-\smallskipamount}\\
\texttt{weakpnt.ml} &  Weak Prime Number Theorem, just for fun \vspace{-\smallskipamount}\\
\texttt{findr.ml} &  use {\small PNT} to provide upper bound on $r$ \vspace{-\smallskipamount}\\
\texttt{aks.ml} &  the actual {\small AKS} theorem
\end{tabular}
\medskip

\green{7814 lines of code, 377 theorems}
\adviwait
\adviplay[slidered]{thefile}
%\adviwait
%\adviplay[slidegreen]{thefilearrow}

\vfill
\end{slide}

\begin{slide}
\slidetitle{$\pi$, $\theta$, $\psi$}
\begin{center}
\begin{tabular}{ccccl}
$\pi(n)$ &=& $\sum_{p\le n} 1$ && counts the primes $\le n$ \\
\red{$\theta(n)$} &\red{=}& \red{$\sum_{p\le n} \ln p$} && sum over all primes $\le n$ \\
$\psi(n)$ &=& $\sum_{p^k\le n} \ln p$ && sum over all prime-powers $\le n$
\end{tabular}
\end{center}
\adviwait
\medskip

\textbf{examples}
\begin{itemize}
\item[]
$\pi(6) = 1 + 1 + 1 = 3$

\item[]
$\theta(6) = \ln(2) + \ln(3) + \ln(5) = \ln(30) = 3.40120$

\item[]
$\psi(6) = \ln(2) + \ln(3) + \ln(2) + \ln(5) = \ln(60) = 4.09434$

\end{itemize}
\adviwait

$$\green{\pi(n)\sim {n\over\ln n} \qquad \theta(n)\sim n \qquad \psi(n)\sim n}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{theta.ml}}
\textbf{1 definition}

\red{$\texttt{theta} \in \texttt{num}\to\texttt{real}$}
\adviwait

\textbf{1 tactic}

\red{\small\texttt{THETA\char`\_LIST}} \verb|:| \verb|int| \verb|->| \verb|thm list| \\
\green{\texttt{[}{\footnotesize $\;\vdash \theta(n) = \ln(\ldots)$}\texttt{;}{\footnotesize $\; \vdash \theta(n - 1) = \ln(\ldots)$}\texttt{;}{\footnotesize $\; \ldots$\,}\texttt{;}{\footnotesize $\; \vdash \theta(0) = \ln(1)\,$}\texttt{]}}

called only once, for $\theta$ lower bound: {\small\verb|THETA_LIST|} \verb|412|
\adviwait

\textbf{12 theorems}

main ones: \red{\small\texttt{PSI\char`\_THETA}}\advirecord{bounds}{, \red{\small\texttt{THETA\char`\_LBOUND\char`\_1\char`\_2}}, \red{\small\texttt{THETA\char`\_UBOUND\char`\_3\char`\_2}}}
$$\theta(n) + \psi(\lfloor\sqrt{n}\rfloor) \le \psi(n) \le \theta(n) + 2\psi(\lfloor\sqrt{n}\rfloor)\adviwait$$
$$\mbox{\llap{$n\ge 5 \;\;\Rightarrow\;\;$}}\, {1\over 2} n \le \theta(n) \le {3\over 2} n\;\;$$
\adviplay{bounds}
\adviwait
\adviembed{/home/freek/talks/intercity/bin/theta}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{{\small\texttt{THETA\char`\_LE\char`\_PSI}}, the smallest proof from \texttt{theta.ml}}
\begin{flushleft}
\advirecord{dim1}{\texttt{let\ }\texttt{THETA\char`\_LE\char`\_PSI}\texttt{ = prove}}\adviplay{dim1} \\
\advirecord{dim2}{\texttt{\ (`}\advirecord{stat}{\texttt{!n.\ theta(n) <= psi(n)}}\adviplay[slidered]{stat}\texttt{`,}}\adviplay{dim2} \\
\verb|  GEN_TAC |\advirecord{then1}{\texttt{THEN}}\adviplay{then1}\verb| REWRITE_TAC[|\advirecord{ref1}{\texttt{theta}}\adviplay{ref1}\verb|; |\advirecord{ref2}{\texttt{psi}}\adviplay{ref2}\verb|] |\advirecord{then2}{\texttt{THEN}}\adviplay{then2} \\
\verb|  MATCH_MP_TAC |\advirecord{ref3}{\texttt{SUM\char`\_LE}}\adviplay{ref3}\verb| |\advirecord{then3}{\texttt{THEN}}\adviplay{then3}\verb| X_GEN_TAC `p:num` |\advirecord{then4}{\texttt{THEN}}\adviplay{then4} \\
\verb|  STRIP_TAC |\advirecord{then5}{\texttt{THEN}}\adviplay{then5}\verb| ASM_CASES_TAC `prime p` |\advirecord{then6}{\texttt{THEN}}\adviplay{then6} \\
\verb|  ASM_REWRITE_TAC[|\advirecord{ref4}{\texttt{MANGOLDT\char`\_POS}}\adviplay{ref4}\verb|] |\advirecord{then7}{\texttt{THEN}}\adviplay{then7} \\
\verb|  ASM_SIMP_TAC[|\advirecord{ref5}{\texttt{mangoldt}}\adviplay{ref5}\verb|; |\advirecord{ref6}{\texttt{PRIME\char`\_PRIMEPOW}}\adviplay{ref6}\verb|] |\advirecord{then8}{\texttt{THEN}}\adviplay{then8} \\
\verb|  SUBGOAL_THEN `aprimedivisor p = p`| \\
\verb|   (fun th -> REWRITE_TAC[th; |\advirecord{ref7}{\texttt{REAL\char`\_LE\char`\_REFL}}\adviplay{ref7}\verb|]) |\advirecord{then9}{\texttt{THEN}}\adviplay{then9} \\
\verb|  ASM_MESON_TAC[|\advirecord{ref8}{\texttt{APRIMEDIVISOR\char`\_PRIMEPOW}}\adviplay{ref8}\verb|; |\advirecord{ref9}{\texttt{EXP\char`\_1}}\adviplay{ref9}\verb|; |\advirecord{ref10}{\texttt{LE\char`\_REFL}}\adviplay{ref10}\verb|]|\advirecord{dim3}{\texttt{);;}}\adviplay{dim3}
\end{flushleft}
\adviwait
\medskip

\adviplay[slidegray]{dim1}
\adviplay[slidegray]{dim2}
\adviplay[slidegray]{stat}
\adviplay[slidegray]{dim3}
\adviwait

\adviplay[slidegreen]{ref1}
\adviplay[slidegreen]{ref2}
\adviplay[slidegreen]{ref3}
\adviplay[slidegreen]{ref4}
\adviplay[slidegreen]{ref5}
\adviplay[slidegreen]{ref6}
\adviplay[slidegreen]{ref7}
\adviplay[slidegreen]{ref8}
\adviplay[slidegreen]{ref9}
\adviplay[slidegreen]{ref10}
\adviwait

\adviplay[slidered]{then1}
\adviplay[slidered]{then2}
\adviplay[slidered]{then3}
\adviplay[slidered]{then4}
\adviplay[slidered]{then5}
\adviplay[slidered]{then6}
\adviplay[slidered]{then7}
\adviplay[slidered]{then8}
\adviplay[slidered]{then9}
\adviwait

HOL proofs are unreadable all-capital `code' \\
%\adviwait
\blue{(if you want formal proofs to be readable: use the Mizar proof assistant)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proving with tactics: the system keeps a `proof obligation'}
\begin{flushleft}
\verb|it : goalstack = 1 subgoal (1 total)|
\end{flushleft}
\begin{flushleft}
\green{\texttt{`!n.\ theta n <= psi n`}}
\end{flushleft}
\begin{flushleft}
\verb|#|\adviwait\verb|e |\red{\texttt{GEN\char`\_TAC}}\verb|;;| \\
\adviwait
\verb|it : goalstack = 1 subgoal (1 total)|
\end{flushleft}
\begin{flushleft}
\green{\texttt{`theta n <= psi n`}}
\end{flushleft}
\begin{flushleft}
\verb|#|\adviwait\verb|e (|\red{\texttt{REWRITE\char`\_TAC[theta; psi]}}\verb|);;| \\
\adviwait
\verb|it : goalstack = 1 subgoal (1 total)|
\end{flushleft}
\green{\texttt{`Sum (1,n) (\char`\\p.\ if prime p then ln (\char`\&p) else \char`\&0) <=}} \\
\green{\texttt{\ Sum (1,n) (\char`\\d.\ mangoldt d)`}}
\begin{flushleft}
\verb|#|\adviwait\verb|e (|\red{\texttt{MATCH\char`\_MP\char`\_TAC SUM\char`\_LE}}\verb|);;| \smallskip\\
\adviwait
\green{\dots}
\end{flushleft}

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

\begin{slide}
\slidetitle{the 10 theorems that the proof refers to}

\begingroup
\footnotesize
\strut$\hspace{-2.5em}$\begin{tabular}{rl}
\advirecord{thm1}{\texttt{theta}}\adviplay{thm1} & \verb/!n. theta n = Sum (1,n)/ \vspace{-\smallskipamount}\\
& \verb/              (\p. if prime p then ln (&p) else &0)/ \\
\advirecord{thm2}{\texttt{psi}}\adviplay{thm2} & \verb/!n. psi n = Sum (1,n) (\d. mangoldt d)/ \\
\verb|SUM_LE| & \verb@!f g m n. (!r. m <= r /\ r < n + m ==> f r <= g r)@ \vspace{-\smallskipamount}\\
& \verb@          ==> Sum (m,n) f <= Sum (m,n) g@ \\
\verb|MANGOLDT_POS| & \verb/!d. &0 <= mangoldt d/ \\
\advirecord{thm3}{\texttt{mangoldt}}\adviplay{thm3} & \verb/!d. mangoldt d =/ \vspace{-\smallskipamount}\\
& \verb/    (if primepow d then ln (&(aprimedivisor d))/ \vspace{-\smallskipamount}\\
& \verb/                   else &0)/ \\
\verb|PRIME_PRIMEPOW| & \verb/!p. prime p ==> primepow p/ \\
\verb|REAL_LE_REFL| & \advirecord{thm4}{\texttt{!x.\ x <= x}}\adviplay{thm4} \\
\verb|APRIMEDIVISOR_PRIMEPOW| & \verb@!p k. prime p /\ 1 <= k@ \vspace{-\smallskipamount}\\
& \verb@      ==> (aprimedivisor (p EXP k) = p)@ \\
\verb|EXP_1| & \verb/!n. n EXP 1 = n/ \\
\verb|LE_REFL| & \advirecord{thm5}{\texttt{!n.\ n <= n}}\adviplay{thm5}
\end{tabular}$\hspace{-3em}$
\endgroup
\adviwait
\adviplay[slidered]{thm1}
\adviplay[slidered]{thm2}
\adviplay[slidered]{thm3}
\adviwait
\adviplay[slidered]{thm4}
\adviplay[slidered]{thm5}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the QED dream of the formalization of mathematics}
\adviwait
\slidetitle{some metrics of proof formalization}
\begin{itemize}
\item[$\bullet$]
\textbf{formalization in space}

formalization is about \red{4 times} as big as informal {\TeX} source \\
\green{`de Bruijn factor'}
%\adviwait
\medskip

\item[$\bullet$]
\textbf{formalization in time}

formalization takes about \red{1 man-week} for a textbook page

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{systems}

the main current proof assistants for the formalization of mathematics
\medskip

\begin{tabular}{ll}
\advirecord{sys1}{HOL Light}\adviplay{sys1} \green{(UK)} & \advirecord{attr1}{the most \red{elegant} system} \\
\advirecord{sys2}{Mizar}\adviplay{sys2} \green{(Poland)} & \advirecord{attr2}{the most \red{mathematical} system} \\
\advirecord{sys3}{Isabelle}\adviplay{sys3} \green{(UK/Germany)} & \advirecord{attr3}{the most \red{all-round} system} \\
\advirecord{sys4a}{Coq}\adviplay{sys4a} \green{(France)} \& \advirecord{sys4b}{NuPRL}\adviplay{sys4b} \green{(US)} & \advirecord{attr4}{the most \red{constructive} systems} \\
\advirecord{sys5}{PVS}\adviplay{sys5} \green{(US)} & \advirecord{attr5}{the most \red{popular} system}
\end{tabular}
\adviwait

\adviplay[slidered]{sys1}\adviplay{attr1}\adviwait
\adviplay[slidered]{sys2}\adviplay{attr2}\adviwait
\adviplay[slidered]{sys3}\adviplay{attr3}\adviwait
\adviplay[slidered]{sys4a}\adviplay[slidered]{sys4b}\adviplay{attr4}\adviwait
\adviplay[slidered]{sys5}\adviplay{attr5}\adviwait

\medskip
\blue{(disclaimer: opinions on these systems may vary)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{so why would anyone want to go to all this trouble?}

uses of formalized mathematics
\begin{itemize}
\item[$\bullet$]
\textbf{checking}

`debugging' proofs
\adviwait

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

making all definitions very precise \\
making scopes of assumptions in proofs explicit \\
finding dependencies between lemmas

\end{itemize}
\adviwait
\medskip

another reason people are doing this (I think)
\begin{itemize}
\item[\red{$\bullet$}]
\red{\textbf{crafting a complex artifact}}

\red{mathematical proof in its purest form}
\end{itemize}


\vfill
\end{slide}

\end{document}