\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,.6}
\definecolor{slidegreen}{rgb}{0,.4,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{.8pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}

\def\headphoto#1{\vbox to 0pt{
\vspace{-0.9em}
\hfill\includegraphics[width=6.5em]{/home/freek/talks/lagrange/pics/people/#1.eps}\par
\vss}\vspace{-1.4em}}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut sketching Lagrange}

\red{Freek Wiedijk} %\\
%Radboud University Nijmegen
\smallskip

\green{Brouwer seminar} \\
Radboud University Nijmegen \\
{\small 2009\hspace{3pt}06\hspace{3pt}09, 15\hspace{1pt}:\hspace{1.8pt}45}

\end{slide}

\begin{slide}
\sectiontitle{a claim about formal mathematics}
\slidetitle{is formalization research?}

\blue{claim}\exclspace:
\begin{center}
\bigskip
\textbf{writing a formalization is laborious, but trivial}
\bigskip
\bigskip
\end{center}

\green{formalization = \\
\red{full} formal proof needing just the axioms of the system}

\vfill
\end{slide}

\begin{slide}
\slidetitle{part 1 of the claim}

\begin{center}
\bigskip
\textbf{turning informal text into formal proof sketch is trivial}
\bigskip
\bigskip
\end{center}

\green{formal proof sketch = \\
rendering of existing proof text in a formal language = \\
\red{incomplete} formalization}

\vfill
\end{slide}

\begin{slide}
\slidetitle{part 2 of the claim}

\begin{center}
\bigskip
\textbf{turning formal proof sketch into full formalization is trivial}
\bigskip
\bigskip
\end{center}

\red{`coloring in'} the formal proof sketch
\bigskip

\green{`coloring in' = \\
adding intermediate steps + \\
adding references between steps + \\
adding references to lemmas from the library}

\vfill
\end{slide}

\begin{slide}
\slidetitle{additional claim}

\begin{center}
\bigskip
\textbf{there is not a `best way' to formalize a theorem}
\bigskip
\bigskip
\end{center}

\green{\red{any} informal presentation is formalizable}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the story of Martijn, Dan, John, Henk and Tonny}
\slidetitle{an exercise for Dan}
\headphoto{martijn}

Martijn's PhD thesis (among many other things): \\
\green{Coq formalization of \red{Fermat's little theorem}}
$$\green{a^{p - 1} \equiv 1\; ({\rm mod}\; p)}\hspace{8em}\medskip\smallskip\adviwait$$

{my proposal to Dan:} \\
\textbf{more `mathematical' formalization\exclspace?}
\smallskip
\begin{itemize}
\item[$\bullet$]
formalize \red{Lagrange's theorem} in C-CoRN
\item[$\bullet$]
prove Fermat's little theorem from Lagrange
\item[$\bullet$]
add everything to C-CoRN
\end{itemize}

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

\begin{slide}
\slidetitle{\textbf{Dan's struggle}}
\headphoto{dan}

\begin{itemize}
\item[$\bullet$]
\blue{constructive finiteness is subtle} \\
e.g., subsets of a finite set not necessarily finite
\medskip

various equivalent \red{definitions of finiteness} \\
\green{`the right definition'?}
\medskip

\item[$\bullet$]
\blue{Lagrange proof needs \red{representants} of cosets} \\
\green{where to get the choice operator\exclspace?}
\medskip
\adviwait

\item[$\bullet$]
\blue{also\exclspace: {setoids} were a pain \adviwait (in those days\exclspace\dots$\!$)}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{John's version}
\headphoto{johnh}

249 lines of \red{HOL Light} code
\vspace{6.5em}

\blue{statement\exclspace:}

\begingroup
\def\\{\char`\\}
\begin{alltt}\small
\green{!g h (**) i e.
    group (g,(**),i,e:A) /\\ subgroup h (g,(**),i,e) /\\ FINITE g\toolong
    ==> ?q. CARD(g) = CARD(q) * CARD(h) /\\
            !b. b IN g ==> ?a x. a IN q /\\ x IN h /\\ b = a**x}\toolong
\end{alltt}
\endgroup

\adviwait
\adviembed{emacs /home/freek/talks/lagrange/lagrange.ml}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Henk's vision}
\headphoto{henk}
\vspace{0\bigskipamount}
$$\mbox{computer mathematics} \;\supseteq\; \mbox{formalization}\hspace{9em}\medskip\smallskip\adviwait$$
$$\mbox{computer mathematics} \;=\; \mbox{formalization}\hspace{9em}\vspace{-\medskipamount}$$
$$\mbox{\phantom{computer mathematics}\phantom{${} \;=\; {}$}\llap{${} \;+\; {}\adviwait$}\rlap{computer algebra}\phantom{formalization}}\hspace{9em}\vspace{-\medskipamount}$$
$$\mbox{\phantom{computer mathematics}\phantom{${} \;=\; {}$}\llap{${} \;+\; {}\adviwait$}\rlap{visualization}\phantom{formalization}}\hspace{9em}\vspace{-\medskipamount}$$
$$\mbox{\phantom{computer mathematics}\phantom{${} \;=\; {}$}\llap{${} \;+\; {}\adviwait$}\rlap{presentation}\phantom{formalization}}\hspace{9em}\vspace{-\medskipamount}$$
$$\mbox{\phantom{computer mathematics}\phantom{${} \;=\; {}$}\llap{${} \;+\; {}\adviwait$}\rlap{exploration}\phantom{formalization}}\hspace{9em}\vspace{-\medskipamount}$$
$$\mbox{\phantom{computer mathematics}\phantom{${} \;=\; {}$}\llap{${} \;+\; {}\adviwait$}\rlap{\dots}\phantom{formalization}}\hspace{9em}$$

\blue{`everything a computer can do for a mathematician, in a unified system'}
\bigskip
\smallskip
\adviwait

\green{Lagrange as a case study\exclspace!}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Tonny's version}
\headphoto{tonny}

\begin{center}
\bigskip
\textbf{`the best way' to formalize Lagrange?}\hspace{8em}\strut
\bigskip
\bigskip
\end{center}

\green{where to go in the space of possible formalizations?}
\smallskip
\begin{itemize}
\item[$\bullet$]
\blue{Tonny's game\exclspace:} nicest way
\item[$\bullet$]
\blue{my game\exclspace:} follow any textbook source
\end{itemize}
\bigskip
\smallskip
\adviwait

\green{(my game covers a bigger part of the space\exclspace\dots$\!$)}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Lagrange's theorem}
\slidetitle{Giuseppe Lodovico Lagrangia}
\headphoto{lagrange}

\begin{center}
\bigskip
\textbf{order of subgroup divides order of the group}\hspace{8em}\strut
\bigskip
\medskip
\end{center}

\green{subgroup = \\
subset closed under group operations}
\smallskip

\green{order = \\ number of elements}
\bigskip
\smallskip
\adviwait

{trivial\exclspace:} \\
\blue{group is partitioned by \red{cosets}, which all have the size of the subgroup}

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

\begin{slide}
\slidetitle{in the top 100}

\begin{quote}
\medskip
\begin{enumerate}
\setcounter{enumi}{70}
\item
\textbf{Order of a Subgroup} \\
HOL Light, \red{John Harrison} \\
Mizar, Wojciech Trybulec \\
Isabelle, Florian Kamm\"uller \\
Coq, \red{almost {C-CoRN}, Dan Synek} \& contrib, Laurent Th\'ery \\
ProofPower, Rob Arthan \\
PVS, NASA library, David Lester
\end{enumerate}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{van der Waerden's version}
\slidetitle{page 26 of Algebra I}
\headphoto{waerden}

\red{the formal proof sketch game\exclspace:}
\medskip
\begin{itemize}
\item[$\bullet$]
select a textbook \green{(trivial)}
\item[$\bullet$]
translate into a formal proof sketch \green{(trivial)}
\item[$\bullet$]
color in the formalization \green{(trivial, but laborious)}
\end{itemize}
\bigskip
\bigskip
\adviwait

\blue{what is a good textbook for Lagrange\exclspace?}

\vfill
\end{slide}

\begin{slide}
\def\pic#1{/home/freek/talks/lagrange/pics/vanderwaerden#1.jpg}%
\adviembed{xviewww \pic{1} \pic{3} \pic{5}}\adviwait[1]%
\slidetitle{the proof in detail}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\advirecord{d1}{Zwei Nebenklassen $a\mathfrak{g}$, $b\mathfrak{g}$ k\"onnen sehr wohl gleich sein, ohne da{\ss}
$a = b$ ist.  Immer dann n\"amlich, wenn $a^{-1}b$ in $\mathfrak{g}$ liegt, gilt
$$b\mathfrak{g} = aa^{-1}b\mathfrak{g} = a(a^{-1}b\mathfrak{g}) = a\mathfrak{g}\exclspace.$$}%
\hspace{\parindent}\advirecord{d2a}{Zwei \textsl{verschiedene} Nebenklassen haben kein Element gemeinsam.}
\advirecord{d2b}{Denn wenn die Nebenklassen $a\mathfrak{g}$ und $b\mathfrak{g}$ ein Element gemein haben, etwa
$$ag_1 = bg_2\exclspace,$$}%
\advirecord{d2c}{so folgt
$$g_1g_2^{-1} = a^{-1}b\exclspace,$$}%
\advirecord{d2d}{so da{\ss} $a^{-1}b$ in $\mathfrak{g}$ liegt;} \advirecord{d2e}{nach dem Vorigen sind also $a\mathfrak{g}$ und $b\mathfrak{g}$ identisch.}
\medskip
\end{tabular}
\end{center}
\vss
}
\adviwait
\adviplay{d1}
\adviwait
\adviplay{d2a}
\adviwait
\adviplay{d2b}
\adviwait
\adviplay{d2c}
\adviwait
\adviplay{d2d}
\adviwait
\adviplay{d2e}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof in detail (continued)}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\advirecord{d3a}{Jedes Element $a$ geh\"ort einer Nebenklasse an, n\"amlich der Neben\-%
klasse $a\mathfrak{g}$.}  \advirecord{d3b}{Diese enth\"alt ja sicher das Element $ae = a$.}  \advirecord{d3c}{Nach dem eben
Bewiesenen geh\"ort das Element $a$ auch \textsl{nur} einer Nebenklasse an.}  \advirecord{d3d}{Wir
k\"onnen demnach jedes Element $a$ als \textsl{Repr\"asentanten} der $a$ enthaltenden
Nebenklass $a\mathfrak{g}$ ansehen.}

\advirecord{d4}{Nach dem vorhergehenden bilden die Nebenklassen eine \textsl{Klassen\-%
einteilung} der Gruppe $\mathfrak{G}$.  Jedes Element geh\"ort einer und nur einer
Klasse an.}

\advirecord{d5}{Je zwei Nebenklassen sind gleichm\"achtig.  Denn durch $a\mathfrak{g} \to b\mathfrak{g}$ ist
eine eineindeutige Abbildung von $a\mathfrak{g}$ auf $b\mathfrak{g}$ definiert.}

\advirecord{d6}{Die Nebenklassen sind, mit Ausnahme von $\mathfrak{g}$ selbst, \textsl{keine} Gruppen;
denn eine Gruppe m\"u{\ss}te das Einselelement enthalten.}
\medskip
\end{tabular}
\end{center}
\vss
}
\adviplay{d3a}
\adviplay{d3b}
\adviwait
\adviplay{d3c}
\adviplay{d3d}
\adviwait
\adviplay{d4}
\adviwait
\adviplay{d5}
\adviwait
\adviplay{d6}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof in detail (continued)}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\advirecord{d7}{Die Anzahl der verschiedenen Nebenklassen einer Untergruppe $\mathfrak{g}$
in $\mathfrak{G}$ hei{\ss}t der \textsl{Index} von $\mathfrak{g}$ in $\mathfrak{G}$.  Der Index kann endlich oder un\-%
endlich sein.}

\advirecord{d8}{Ist $N$ die als (endlich angenommene) Ordnung von $\mathfrak{G}$, $n$ die von $\mathfrak{g}$,
$j$~der Index, so gilt die Relation
$$N = jn\exclspace;\leqno{\hspace{.3em}(2)}$$
denn $\mathfrak{G}$ ist ja in $j$ Klassen eingeteilt, deren jede $n$ Elemente enth\"alt.}

\advirecord{d9}{Man kann f\"ur endliche Gruppen aus (2) den Index $j$ berechnen:
$$j = {N\over n}\exclspace.\smallskip$$}%
\hspace{\parindent}\advirecord{d10}{\textbf{Folge.}  \textsl{Die Ordnung einer Untergruppe einer endlichen Gruppe ist
ein Teiler der Ordnung der Gesamtgruppe.}}
\medskip
\end{tabular}
\end{center}
\vss
}
\adviplay{d7}
\adviwait
\adviplay{d8}
\adviwait
\adviplay{d9}
\adviwait
\adviplay{d10}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{sketching the proof}
\slidetitle{the formal proof sketch}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\vspace{1.0em}
\white{\advirecord{c1}{Zwei Nebenklassen $a\mathfrak{g}$, $b\mathfrak{g}$ k\"onnen sehr wohl gleich sein, ohne da{\ss}
$a = b$ ist.  Immer dann n\"amlich, wenn $a^{-1}b$ in $\mathfrak{g}$ liegt, gilt
$$b\mathfrak{g} = aa^{-1}b\mathfrak{g} = a(a^{-1}b\mathfrak{g}) = a\mathfrak{g}\exclspace.$$}}

\vspace{-2.15em}
\white{\advirecord{c2}{Zwei \textsl{verschiedene} Nebenklassen haben kein Element gemeinsam.
Denn wenn die Nebenklassen $a\mathfrak{g}$ und $b\mathfrak{g}$ ein Element gemein haben, etwa
$$ag_1 = bg_2\exclspace,$$
so folgt
$$g_1g_2^{-1} = a^{-1}b\exclspace,$$
so da{\ss} $a^{-1}b$ in $\mathfrak{g}$ liegt; nach dem Vorigen sind also $a\mathfrak{g}$ und $b\mathfrak{g}$ identisch.}}
\end{tabular}
\end{center}
\vss
}
\vbox to 0pt{
\vspace{-2.5em}
\begin{center}
\begin{tabular}{|p{9cm}|}
\small
\rightskip .2em plus 2em
\parindent=0em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-1.25em}
\advirecord{b0}{\hbox{}\texttt{now let H,G;}} \hfill\break
\advirecord{b1}{\hbox{}\texttt{\ now let a,b;} \hfill\break
\hbox{}\texttt{\ \ assume a\char`\^-1*b in G;} \hfill\break
\hbox{}\texttt{\ \ thus b*G = a*a\char`\^-1*b*G .= a*(a\char`\^-1*b*G) .= a*G;}\toolong \hfill\break
\hbox{}\texttt{\ end;}} \hfill\break
\advirecord{b2}{\hbox{}\texttt{\ for a,b st a*G <> b*G holds (a*G) /\char`\\\ (b*G) = \char`\{\char`\}}\toolong \hfill\break
\hbox{}\texttt{\ proof let a,b;} \hfill\break
\hbox{}\texttt{\ \ now assume (a*G) /\char`\\\ (b*G) <> \char`\{\char`\};} \hfill\break
\hbox{}\texttt{\ \ \ consider g1,g2 such that a*g1 = b*g2;}} \hfill\break
\advirecord{b3}{\hbox{}\texttt{\ \ \ g1*g2\char`\^-1 = a\char`\^-1*b;} \hfill\break
\hbox{}\texttt{\ \ \ a\char`\^-1*b in G;} \hfill\break
\hbox{}\texttt{\ \ \ thus a*G = b*G;} \hfill\break
\hbox{}\texttt{\ \ end;} \hfill\break
\hbox{}\texttt{\ \ thus thesis;} \hfill\break
\hbox{}\texttt{\ end;}}
\medskip
\end{tabular}
\end{center}
\adviwait
\adviplay{b0}
\adviwait
\adviplay[slidegray]{c1}
\adviwait
\adviplay[white]{c1}
\adviplay{b1}
\adviwait
\adviplay[slidegray]{c2}
\adviwait
\adviplay[white]{c2}
\adviplay{b2}
\adviplay{b3}
\adviwait
\adviplay[slidered]{b2}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the formal proof sketch (continued)}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\vspace{-.1em}
\white{\advirecord{c3}{Jedes Element $a$ geh\"ort einer Nebenklasse an, n\"amlich der Neben\-%
klasse $a\mathfrak{g}$.  Diese enth\"alt ja sicher das Element $ae = a$.  %Nach dem eben
%Bewiesenen geh\"ort das Element $a$ auch \textsl{nur} einer Nebenklasse an.  Wir
%k\"onnen demnach jedes Element $a$ als \textsl{Repr\"asentanten} der $a$ enthaltenden
%Nebenklass $a\mathfrak{g}$ ansehen.
}}

\vspace{2em}
\white{\advirecord{c4}{Nach dem vorhergehenden bilden die Nebenklassen eine \textsl{Klassen\-%
einteilung} der Gruppe $\mathfrak{G}$.  Jedes Element geh\"ort einer und nur einer
Klasse an.}}

\vspace{-2.6em}
\white{\advirecord{c5}{Je zwei Nebenklassen sind gleichm\"achtig.  Denn durch $a\mathfrak{g} \to b\mathfrak{g}$ ist
eine eineindeutige Abbildung von $a\mathfrak{g}$ auf $b\mathfrak{g}$ definiert.}}
\end{tabular}
\end{center}
\vss
}
\vbox to 0pt{
\vspace{-2.6em}
\begin{center}
\begin{tabular}{|p{9cm}|}
\small
\rightskip .2em plus 2em
\parindent=0em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-1.1em}
\advirecord{b4}{\hbox{}\texttt{\ for a holds a in a*G} \hfill\break
\hbox{}\texttt{\ proof let a;} \hfill\break
\hbox{}\texttt{\ \ a*e(G) = a;} \hfill\break
\hbox{}\texttt{\ \ thus thesis;} \hfill\break
\hbox{}\texttt{\ end;}} \hfill\break
\advirecord{b5}{\hbox{}\texttt{\ \char`\{a*G :\ a in H\char`\}\ is a\char`\_partition of H;}} \hfill\break
\advirecord{b6}{\hbox{}\texttt{\ for a,b holds card(a*G) = card(b*G)} \hfill\break
\hbox{}\texttt{\ proof let a,b;} \hfill\break
\hbox{}\texttt{\ \ consider f being Function of a*G,b*G such that}\toolong \hfill\break
\hbox{}\texttt{\ \ \ for g holds f.(a*g) = b*g;} \hfill\break
\hbox{}\texttt{\ \ f is bijective;} \hfill\break
\hbox{}\texttt{\ \ thus thesis;} \hfill\break
\hbox{}\texttt{\ end;}}
\medskip
\end{tabular}
\end{center}
\adviplay[slidegray]{c3}
\adviwait
\adviplay[white]{c3}
\adviplay{b4}
\adviwait
\adviplay[slidegray]{c4}
\adviwait
\adviplay[white]{c4}
\adviplay{b5}
\adviwait
\adviplay[slidegray]{c5}
\adviwait
\adviplay[white]{c5}
\adviplay{b6}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the formal proof sketch (continued)}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{|p{9cm}|}
%\rm
\rightskip .2em plus 2em
\parindent=1.2em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.4em}
\vspace{-.2em}
\white{\advirecord{c6}{Die Anzahl der verschiedenen Nebenklassen einer Untergruppe $\mathfrak{g}$
in $\mathfrak{G}$ hei{\ss}t der \textsl{Index} von $\mathfrak{g}$ in $\mathfrak{G}$.  %Der Index kann endlich oder un\-%
%endlich sein.
}}

\vspace{-1.35em}
\white{\advirecord{c7}{Ist $N$ die als (endlich angenommene) Ordnung von $\mathfrak{G}$, $n$ die von $\mathfrak{g}$,
$j$~der Index, so gilt die Relation
$$N = jn\exclspace;\leqno{\hspace{.3em}(2)}$$
denn $\mathfrak{G}$ ist ja in $j$ Klassen eingeteilt, deren jede $n$ Elemente enth\"alt.}}

%Man kann f\"ur endliche Gruppen aus (2) den Index $j$ berechnen:
%$$j = {N\over n}\exclspace.\vspace{1.0\smallskipamount}$$

\vspace{-.9em}
\white{\advirecord{c8}{\textbf{Folge.}  \textsl{Die Ordnung einer Untergruppe einer endlichen Gruppe ist
ein Teiler der Ordnung der Gesamtgruppe.}}}
\end{tabular}
\end{center}
\vss
}
\vbox to 0pt{
\vspace{-2.6em}
\begin{center}
\begin{tabular}{|p{9cm}|}
\small
\rightskip .2em plus 2em
\parindent=0em
\baselineskip=1.25em
\leftskip=.3em
\vspace{-.6em}
\vspace{-.6em}
\advirecord{b7}{\hbox{}\texttt{\ set 'Index' = card \char`\{a*G :\ a in H\char`\};}} \hfill\break
\advirecord{b8}{\hbox{}\texttt{\ now} \hfill\break
\hbox{}\texttt{\ \ let N such that N = card H;} \hfill\break
\hbox{}\texttt{\ \ let n such that n = card G;} \hfill\break
\hbox{}\texttt{\ \ let j such that j = 'Index';} \hfill\break
\hbox{}\texttt{\ \ thus '2':\ N = j*n;} \hfill\break
\hbox{}\texttt{\ end;}} \hfill\break
\advirecord{b9}{\hbox{}\texttt{\ thus card G divides card H;} \hfill\break
\hbox{}\texttt{end;}}
\medskip
\end{tabular}
\end{center}
\vss
}
\adviplay[slidegray]{c6}
\adviwait
\adviplay[white]{c6}
\adviplay{b7}
\adviwait
\adviplay[slidegray]{c7}
\adviwait
\adviplay[white]{c7}
\adviplay{b8}
\adviwait
\adviplay[slidegray]{c8}
\adviwait
\adviplay[white]{c8}
\adviplay{b9}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the formalization}
\slidetitle{filling in a fragment of the full proof}
\vbox to 0pt{
\vspace{-1em}
\begingroup
\def\xxx{\baselineskip=1.25em}%
\def\\{\char`\\}%
\def\{{\char`\{}%
\def\}{\char`\}}%
\begin{alltt}\small\xxx
\green{\advirecord{a1}{A3:}} for a,b st a*G <> b*G holds (a*G) /\\ (b*G) = \{\}
 proof let a,b;
  now assume (a*G) /\\ (b*G) <> \{\};
   \blue{\advirecord{a2}{\green{\advirecord{a2w}{then}} \red{\advirecord{a2a}{consider x such that}}
\green{\advirecord{a2x}{A4:}} \red{\advirecord{a2b}{x in (a*G) /\\ (b*G)}} by XBOOLE_0:7\red{\advirecord{a2c}{;}}
\green{\advirecord{a2y}{A5:}} \red{\advirecord{a2d}{x in a*G & x in b*G}} \green{\advirecord{a2z}{by A4}},XBOOLE_0:def 4\red{\advirecord{a2e}{;}}}}
   consider g1\white{\advirecord{a6}{,}}\blue{\advirecord{a3}{\red{\advirecord{a3a}{such that}}
\green{\advirecord{a3x}{A6:}} \red{\advirecord{a3b}{x = a*g1}} \green{\advirecord{a3y}{by A5}},Th5\red{\advirecord{a3c}{;
   consider}}}} g2 such that
\blue{\advirecord{a4}{\green{\advirecord{a4x}{A7:}} \red{\advirecord{a4a}{x = b*g2}} \green{\advirecord{a4y}{by A5}},Th5\red{\advirecord{a4b}{;
   set g1G = g1;
   set g2G = g2;
   reconsider g1 as Element of H}} by GROUP_2:51\red{\advirecord{a4c}{;
   reconsider g2 as Element of H}} by GROUP_2:51\red{\advirecord{a4d}{;}}
\green{\advirecord{a4z}{A8:}}}} a*g1 = \blue{\advirecord{a4}{\red{\advirecord{a4a}{a*g1G}} by Th2
    \red{\advirecord{a4b}{.=}}}} b*g2 \blue{\advirecord{a5}{\green{\advirecord{a5x}{by A6,A7}},Th2}};
\end{alltt}
\endgroup
\adviplay{a6}
\adviwait
\adviplay[white]{a6}
\adviplay[slidered]{a2a}
\adviplay[slidered]{a2b}
\adviplay[slidered]{a2c}
\adviplay[slidered]{a2d}
\adviplay[slidered]{a2e}
\adviplay[slidered]{a3a}
\adviplay[slidered]{a3b}
\adviplay[slidered]{a3c}
\adviplay[slidered]{a4a}
\adviplay[slidered]{a4b}
\adviplay[slidered]{a4c}
\adviplay[slidered]{a4d}
\adviplay[slidered]{a4a}
\adviplay[slidered]{a4b}
\adviwait
\adviplay[slidegreen]{a1}
\adviplay[slidegreen]{a2w}
\adviplay[slidegreen]{a2x}
\adviplay[slidegreen]{a2y}
\adviplay[slidegreen]{a2z}
\adviplay[slidegreen]{a3x}
\adviplay[slidegreen]{a3y}
\adviplay[slidegreen]{a4x}
\adviplay[slidegreen]{a4y}
\adviplay[slidegreen]{a4z}
\adviplay[slidegreen]{a5x}
\adviplay[slidegreen]{a5y}
\adviwait
\adviplay[slideblue]{a2}
\adviplay[slideblue]{a3}
\adviplay[slideblue]{a4}
\adviplay[slideblue]{a5}
\adviwait
\adviplay{a2a}
\adviplay{a2b}
\adviplay{a2c}
\adviplay{a2d}
\adviplay{a2e}
\adviplay{a3a}
\adviplay{a3b}
\adviplay{a3c}
\adviplay{a4a}
\adviplay{a4b}
\adviplay{a4c}
\adviplay{a4d}
\adviplay{a4a}
\adviplay{a4b}
\adviplay{a1}
\adviplay{a2w}
\adviplay{a2x}
\adviplay{a2y}
\adviplay{a2z}
\adviplay{a3x}
\adviplay{a3y}
\adviplay{a4x}
\adviplay{a4y}
\adviplay{a4z}
\adviplay{a5x}
\adviplay{a5y}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviplay{a5}
\vss}

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

\begin{slide}
\slidetitle{the collection}

\adviwait
\adviembed{gv -g 1113x781+-89+-28 -spartan -nocenter -scale=1 /home/freek/web/freek/notes/sketches1.ps.gz}\adviwait[1]%

\vspace{-1.85em}
\textsl{for every formal proof sketch\exclspace:}
\smallskip
\begin{itemize}
\item[$\bullet$]
source of the informal proof
\item[$\bullet$]
text of the informal proof
\item[$\bullet$]
formal proof sketch\exclspace: \red{informal layout}
\item[$\bullet$]
formal proof sketch\exclspace: \red{formal layout} \\
\green{with errors marked in the margin}
\item[$\bullet$]
full formal proof \\
\green{with formal proof sketch part underlined}
\item[$\bullet$]
Mizar version used
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Lagrange formalization \textbf{live}}

444 lines of \red{Mizar} code

only \red{${1\over 3}$rd of the file} corresponds to the sketch
\bigskip
\adviwait

\blue{2 definitions + 7 lemmas, including\exclspace:}
\smallskip

\begin{alltt}\small
\green{for X being finite non empty set, P being a_partition of X,
    n being natural number st
  for A being set st A in P holds card A = n
holds card X = (card P)*n;}
\end{alltt}
\medskip
\adviwait

proof of this one lemma takes about \red{${1\over 4}$th of the file}

\adviwait
\adviembed{emacs +68 /home/freek/math/lagrange/text/sketch.miz}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{de Bruijn factors}
\slidetitle{de Bruijn factor in time}
\headphoto{debruijn}

$${\mbox{1 full \red{week} of work}\over\mbox{1 textbook \red{page}}}\hspace{8em}\bigskip\medskip$$

\green{in this case\exclspace: \red{a bit smaller}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{de Bruijn factor in space}

$${\mbox{size of formalization}\over\mbox{size of textbook}} \approx 4\bigskip$$

\green{in this case: \hspace{10.72em}\red{factor $\approx$ {{1.3}}}}
\bigskip
\adviwait

\blue{specifics of the de Bruijn factor game\exclspace:}
\adviwait

\begin{itemize}
\item[$\bullet$]
\textsl{gzip both source and translation} \\
\adviwait
otherwise: factor $\approx$ 1.7
\adviwait

\item[$\bullet$]
\textsl{only count the part of the formalization that parallels the source} \\
\adviwait
otherwise: factor $\approx$ 3.3
\adviwait

\item[]
otherwise both: factor $\approx$ 5.2
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the good news and the bad news}
\slidetitle{the good news: definitions do not matter}

it seems\exclspace:
\begin{center}
\bigskip
\textbf{one can sketch \red{any} textbook proof}
\bigskip
\bigskip
\end{center}

\green{(importance of choice of definitions is an artefact of type theory)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the good news: a good library really helps}

\green{why did Dan have such a hard time?}
\medskip
\begin{itemize}
\item[$\bullet$]
constructive complications
\smallskip
\item[$\bullet$]
\red{not a good library} about counting finite sets
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the bad news: I faked it a bit}

\green{elements of the subgroup are also elements of the group}
\medskip

\blue{Mizar is not flexible enough to handle this transparantly
\adviwait
(nor is Coq)} \\
\adviwait
\gray{maybe using non-\texttt{struct} types for groups helps\exclspace?}
\bigskip
\medskip
\adviwait

\textbf{two approaches\exclspace:}
\smallskip
\begin{itemize}
\item[$\bullet$]
explicit operation \texttt{[g]} that embeds the subgroup
\adviwait
\item[$\bullet$]
\green{define \red{new} operation \texttt{h*g} for `$\,$\texttt{h*[g]}'}
\end{itemize}
\medskip
\smallskip
\adviwait

I used the second approach (for cosmetic reasons)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{one more thing to try}
\slidetitle{porting the sketch}
\advirecord{z}{\headphoto{james}}

\green{Mizar Light III = \\
Mizar proof language on top of HOL Light}
\medskip

\begin{flushright}
\rightskip=10em
{with Mizar Light III it will become possible to \\ \red{generate} Mizar-style proofs by executing tactics}
\end{flushright}
\bigskip
\adviwait

\textsl{\blue{James' proposal\exclspace:}}\adviplay{z}
\begin{center}
\smallskip
\textbf{play the same game in Mizar Light III\exclspace!}\hspace{8em}
\bigskip
\medskip
\end{center}
\adviwait

\gray{but\exclspace: algebra in HOL not very nice$\,$\dots\adviwait \\
but\exclspace: I expect that will not really matter much for my game}

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

\end{document}