\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}{.6,.6,.6}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.92,.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\darkgray#1{\textcolor{slidedarkgray}{#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{-4em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large formalization of mathematics}

Freek Wiedijk \\
Radboud University Nijmegen

\red{{\small TYPES} Summer School 2005} \\
G\"oteborg, Sweden \\
2005 08 23, 11:10
\end{slide}

\begin{slide}
\sectiontitle{intro}
\slidetitle{the best of two worlds}
formalization of mathematics is like:

\begin{itemize}
\item[$\bullet$]
\textbf{computer programming}
\smallskip

\advirecord{a2a}{
\green{concrete, explicit}
}
\advirecord{a1a}{
\\ a {formalization} is much like a \red{computer program}
}
\smallskip
\smallskip

\item[$\bullet$]
\textbf{doing mathematics}
\smallskip

\advirecord{a2b}{
\green{abstract, non-trivial}
}
\advirecord{a1b}{
\\ a {formalization} is much like a \red{mathematical textbook}
}

\end{itemize}
\medskip

you will like it only if you like \textbf{both} programming and mathematics\adviwait
\adviplay{a1a}
\adviplay{a1b}
\adviplay{a2a}
\adviplay{a2b}
\adviwait
\\
\blue{but in that case you will like it very very much!}

\vfill
\end{slide}

\def\qed{{\small QED}}

\begin{slide}
\slidetitle{table of contents: the two parts of this talk}

\begin{description}
\item[\textsf{\textbf{\blue{first hour:}}}]
an overview of \\ the current \red{state of the art} in formalization of mathematics
\medskip

\advirecord{b1}{in the reader: \green{{\qed} manifesto}}
\medskip

\item[\textsf{\textbf{\blue{second hour:}}}]
an overview of \\ \red{Mizar}, the most `mathematical' proof assistant
\medskip

\advirecord{b2}{in the reader: \green{Mizar tutorial}}
\medskip

\end{description}
\adviwait
\adviplay[slidegreen]{b1}
\adviwait
\adviplay[slidegreen]{b2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\Large first hour: \\
\red{state of the art} in formalization of mathematics}
\end{slide}

\begin{slide}
\sectiontitle{mathematics in the computer}
\slidetitle{four ways to do mathematics in the computer}

\begin{itemize}
\item[$\bullet$] \textbf{numerical mathematics}\advirecord{c7}{, \green{experimentation, visualisation}}
\begin{center}
\advirecord{c1}{calculations}\advirecord{c2}{\llap{numbers}}\adviplay[slidegreen]{c1}: computer $\to$ human
\end{center}

\advirecord{c6}{
\item[$\bullet$] \textbf{computer algebra}
\begin{center}
\advirecord{c3}{calculations}\advirecord{c4}{\llap{formulas}}\adviplay[slidegreen]{c3}: computer $\to$ human
\end{center}
}

\item[$\bullet$] \textbf{automated theorem provers}
\begin{center}
\strut\phantom{calculations}\advirecord{c8}{\llap{proofs}}\adviplay[slidegreen]{c8}: \advirecord{c9}{computer $\to$ human}\adviplay{c9}
\end{center}
\adviwait
\adviplay[black]{c8}
\adviplay{c6}
\adviwait
\adviplay[white]{c1}
\adviplay[slidegreen]{c2}
\adviplay[white]{c3}
\adviplay[slidegreen]{c4}
\adviwait
\adviplay[black]{c2}
\adviplay[black]{c4}
\adviplay[slidegreen]{c9}

\item[$\bullet$] \textbf{\advirecord{c5}{proof assistants}\adviplay{c5}}
\begin{center}
\strut\phantom{calculations}\llap{proofs}: \advirecord{c10}{human $\to$ computer}\adviplay[slidegreen]{c10}
\end{center}

\end{itemize}
\adviwait
\adviplay[black]{c9}
\adviplay[black]{c10}
\adviplay[slidered]{c5}
\adviwait
\adviplay{c7}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{numerical mathematics:} Merten's conjecture}
M{\"o}bius function:
$$
\mu(n) =
\left\{
\begin{array}{rl}
0 & \mbox{when $n$ has duplicate prime factors} \\
1 & \mbox{when $n$ has an even number of different prime factors} \\
-1 & \mbox{when $n$ has an odd number of different prime factors}
\end{array}
\right.
\hspace{-3em}
$$
\vspace{-\bigskipamount}
$$\big| \sum_{k = 1}^n \mu(n) \big| < \sqrt{n}\mbox{\quad ?} \mbox{\phantom{Mertens, 1897:}} \leqno{\mbox{Mertens, 1897:}}$$

\vbox to 0pt{
\begin{center}
\quad
\includegraphics[height=8em]{/home/freek/talks/dagen/pics/mimg2409.eps}
\qquad
\includegraphics[height=8em]{/home/freek/talks/dagen/pics/mimg1757.eps}
$\hspace{-1em}$
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Merten's conjecture (continued)}
Odlyzko \& te Riele, 1985: Mertens conjecture is \red{false!} \\
\green{50 uur computer time}
\smallskip

first $n$ where it fails has tens of digits \\
indirect proof!
\smallskip
\adviwait

\green{2000 zeroes of the Riemann zeta function to 100 decimals precision}

\vbox to 0pt{
\tiny
14.1347251417346937904572519835624702707842571156992431756855674601499634298092567649490103931715610127\dots$\hspace{-12em}$ \\
21.0220396387715549926284795938969027773343405249027817546295204035875985860688907997136585141801514195\dots$\hspace{-12em}$ \\
25.0108575801456887632137909925628218186595496725579966724965420067450920984416442778402382245580624407\dots$\hspace{-12em}$ \\
30.4248761258595132103118975305840913201815600237154401809621460369933293893332779202905842939020891106\dots$\hspace{-12em}$ \\
32.9350615877391896906623689640749034888127156035170390092800034407848156086305510059388484961353487245\dots$\hspace{-12em}$ \\
37.5861781588256712572177634807053328214055973508307932183330011136221490896185372647303291049458238034\dots$\hspace{-12em}$ \\
40.9187190121474951873981269146332543957261659627772795361613036672532805287200712829960037198895468755\dots$\hspace{-12em}$ \\
43.3270732809149995194961221654068057826456683718368714468788936855210883223050536264563493710631909335\dots$\hspace{-12em}$ \\
48.0051508811671597279424727494275160416868440011444251177753125198140902164163082813303353723054009977\dots$\hspace{-12em}$ \\
49.7738324776723021819167846785637240577231782996766621007819557504335116115157392787327075074009313300\dots$\hspace{-12em}$ \\
52.9703214777144606441472966088809900638250178888212247799007481403175649503041880541375878270943992988\dots$\hspace{-12em}$ \\
56.4462476970633948043677594767061275527822644717166318454509698439584752802745056669030113142748523874\dots$\hspace{-12em}$ \\
59.3470440026023530796536486749922190310987728064666696981224517547468001526996298118381024870746335484\dots$\hspace{-12em}$ \\
60.8317785246098098442599018245240038029100904512191782571013488248084936672949205384308416703943433565\dots$\hspace{-12em}$ \\
65.1125440480816066608750542531837050293481492951667224059665010866753432326686853844167747844386594714\dots$\hspace{-12em}$ \\
67.0798105294941737144788288965222167701071449517455588741966695516949012189561969835302939750858330343\dots$\hspace{-12em}$ \\
69.5464017111739792529268575265547384430124742096025101573245399996633876722749104195333449331783403563\dots$\hspace{-12em}$ \\
72.0671576744819075825221079698261683904809066214566970866833061514884073723996083483635253304121745329\dots$\hspace{-12em}$ \\
75.7046906990839331683269167620303459228119035306974003016477753015741970277063236083840370218346527980\dots$\hspace{-12em}$ \\
77.1448400688748053726826648563046370157960324492344610417652314531511391642537150894082886946997377597\dots$\hspace{-12em}$ \\
79.3373750202493679227635928771162281906132467431200308784387204971015419326770909746774519946121241090\dots$\hspace{-12em}$ \\
82.9103808540860301831648374947706094975088805937821491465713062832359290863566190755125631923348968187\dots$\hspace{-12em}$ \\
\dots
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{computer algebra:} symbolic integration of
\hbox to 0pt{\vbox to 0pt{\vss$\displaystyle \int_0^\infty {e^{-(x-1)^2}\over\sqrt{x}} dx$}\hss}}
\begin{alltt}\adviwait
> int(exp(-(x-t)^2)/sqrt(x), x=0..infinity);\adviwait
\end{alltt}
$$\green{{1\over 2} {e^{-t^2} \Big({-{3 (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{3\over 4\rlap{\phantom{\tiny g}}}({t^2\over 2}) \over t^{2\rlap{\phantom{x}}}}} + {\textstyle (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{7\over 4}({t^2\over 2})} \Big) \over \pi^{1\over 2}}}\adviwait$$
\begin{alltt}
> subs(t=1,%);\adviwait
\end{alltt}
$$\green{{1\over 2} {e^{-1} \big({-3 \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{3\over 4}({1\over 2})} + \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{7\over 4}({1\over 2})\big) \over \pi^{1\over 2}}}\adviwait$$
\begin{alltt}
> evalf(%);
\end{alltt}
$$\advirecord{d1}{0.4118623312}\adviplay[slidegreen]{d1}\adviwait$$
\begin{alltt}
> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));\adviwait
\end{alltt}
$$\advirecord{d2}{1.973732150}\hspace{.5em}\adviplay[slidegreen]{d2}%\adviwait
%\adviplay[slidered]{d1}
%\adviplay[slidered]{d2}
$$

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

\begin{slide}
\slidetitle{\textbf{automated theorem proving:} Robbins' conjecture}
computers \\
\dashskip {\dots} can in the near future play chess better than a human \\
\adviwait
\dashskip {\dots} can in the near future \red{do mathematics better than a human?}
%\bigskip
\medskip
\adviwait

\begin{tabular}{rl}
Robbins, 1933: & is every \green{Robbins algebra} a \green{Boolean algebra}? \\\adviwait
\textbf{\small EQP}, 1996: & \textbf{yes!} \\
\noalign{\vspace{-\smallskipamount}}
& eight days of computer time
\end{tabular}
\medskip
\adviwait

one of the very few proofs that has first been found by a computer \\
not very conceptual: just searches through very many possibilities

\bigskip
\adviwait

\red{{interesting research, but currently not relevant for mathematics}}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the {\qed} manifesto}
\slidetitle{let's formalize all of mathematics!}
\textbf{{\qed} manifesto}, 1994:
\begin{quote}
\green{
{\qed} is the very tentative title of a project to
build a computer system that effectively rep%-
resents all important mathematical knowledge
and techniques.
}
\medskip
\end{quote}
%\adviwait
pamphlet by anonymous group, led by Bob Boyer \\
\red{utopian vision} %\\
%interesting answers to twelve possible objections

\adviwait
\medskip
{proposed many times} \\
\red{\textbf{never got very far} \adviwait (yet)} \\
%\adviwait
%\textbf{why?}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the two kinds of computer proof}

\begin{itemize}
\item[$\bullet$]
\textbf{correctness of computer software and hardware}

\green{(serious branch of computer science: `formal methods')}
\smallskip

statements: big \\
proofs: shallow \\
computer does the main part of the proof
\bigskip
%\adviwait

\item[$\bullet$]
\textbf{correctness of \advirecord{e}{mathematical theorems}\adviplay{e}}

\green{(slow and thorough style of doing mathematics, still in its infancy)}
\smallskip

statements: small \\
proofs: deep \\
human does the main part of the proof

\end{itemize}
%\adviwait
%\adviplay[slidered]{e}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{a brief overview of proof assistants for mathematics}
\slidetitle{four prehistorical systems}
\begin{center}
\begin{tabular}{rl}
1968 & \textbf{Automath} \\
& Netherlands, de Bruijn \\
\noalign{\medskip}
1971 & \textbf{nqthm} \\
& US, Boyer \& Moore \\
\noalign{\medskip}
1972 & \textbf{LCF} \\
& UK, Milner \\
\noalign{\medskip}
1973 & \textbf{Mizar} \\
& Poland, Trybulec
\end{tabular}
$\qquad$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{seven current systems for mathematics}
\vspace{-2\bigskipamount}

\begingroup
\small
$$\hspace{-8.5em}\xymatrix{
\txt{\advirecord{f1}{Mizar}\adviplay{f1}}\ar@(dr,ul)[rrrd]\ar@{.}[rrrr] &&&& \txt{\rlap{\green{\textsl{most mathematical}}}} \\
\txt{\gray{LCF}}\ar[rr]\ar[rrd]\ar@/_1.8pc/[rrrdd] && \txt{HOL}\ar[r] & \txt{\advirecord{f2}{Isabelle}\adviplay{f2}}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most
pure}}}} \\
\txt{\gray{Automath}}\ar[rr] && \txt{$\,$\advirecord{f3}{\rlap{Coq}\phantom{NuPRL}}\adviplay{f3} \\\noalign{\smallskip} NuPRL$\!$}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most logical}}}} \\
&&& \txt{PVS}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most popular}}}} \\
\txt{\gray{nqthm}}\ar[rr]\ar@/^.5pc/[rrru] && \txt{ACL2}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most computational}}}} \\
}
\adviwait
\adviplay[slidered]{f1}
\adviplay[slideblue]{f2}
\adviplay[slideblue]{f3}
$$
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{a `top 100' of mathematical theorems}

\begingroup
\setlength{\tabcolsep}{2pt}
\def\arraystretch{1}
\begin{tabular}{rl}
1. & \advirecord{g2}{The Irrationality of the Square Root of 2}\adviplay{g2} \advirecord{g3}{\enskip $\leftarrow$ \textsl{all systems}} \\
2. & Fundamental Theorem of Algebra \advirecord{g4}{\enskip $\leftarrow$ Mizar, HOL, Coq} \\
3. & The Denumerability of the Rational Numbers \advirecord{g5}{\enskip $\leftarrow$ Mizar, HOL, Isabelle}\toolong \\
4. & Pythagorean Theorem \advirecord{g6}{\enskip $\leftarrow$ Mizar, HOL, Coq} \\
5. & Prime Number Theorem \advirecord{g7}{\enskip $\leftarrow$ Isabelle} \\
6. & G\"odel's Incompleteness Theorem \advirecord{g8}{\enskip $\leftarrow$ HOL, Coq, nqthm} \\
7. & Law of Quadratic Reciprocity \advirecord{g9}{\enskip $\leftarrow$ Isabelle, nqthm} \\
8. & The Impossibility of Trisecting the Angle and Doubling the Cube \advirecord{g10}{\enskip $\leftarrow$ HOL}\toolong \\
9. & \rlap{\advirecord{g12}{The Area of a Circle}}\advirecord{g1}{\textsl{The Area of a Circle}}\adviplay{g12} \\
10. & Euler's Generalization of Fermat's Little Theorem \advirecord{g11}{\enskip $\leftarrow$ Mizar, HOL, Isabelle}\toolong \\
\dots & \dots
\end{tabular}
\endgroup
\adviwait

\begin{center}
\green{63\% formalized} \\
\adviplay[white]{g12}
\adviplay{g1}
\adviplay[slidered]{g3}
\adviplay[slidered]{g4}
\adviplay[slidered]{g5}
\adviplay[slidered]{g6}
\adviplay[slidered]{g7}
\adviplay[slidered]{g8}
\adviplay[slidered]{g9}
\adviplay[slidered]{g10}
\adviplay[slidered]{g11}
\adviwait
\blue{\url{http://www.cs.ru.nl/~freek/100/}}
\end{center}

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

\begin{slide}
\slidetitle{\textbf{(advertisement)}\enskip the seventeen provers of the world}

\begin{center}
\textbf{LNAI 3600}
\end{center}

one theorem \\
seventeen formalisations \advirecord{h}{$+$ explanations about the systems}
\bigskip

\begin{center}
\red{HOL, Mizar, PVS, Coq, Otter, Isabelle, Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Lego, NuPRL, $\Omega$mega, B method, Minlog}
\bigskip
\end{center}
\adviwait
\adviplay[slidegray]{h}
\adviwait

\begin{center}
\blue{\url{http://www.cs.ru.nl/~freek/comparison/}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{state of the art: recent big formalizations}
\slidetitle{Prime Number Theorem}
Bob Solovay's challenge:
\begin{quote}
\red{
I suspect that
fully formalizing the \advirecord{i1}{\rlap{usual proof of the prime}}\advirecord{i2}{{\textbf{usual} proof of the prime}}\adviplay{i1}
number theorem \black{[\dots$\!$]} is
beyond the current capacities of the \black{[}formalization\black{]} community.  Say within the next
ten years.
}
\end{quote}
\adviwait
\medskip

Jeremy Avigad e.a.:
\begin{quote}
\begin{alltt}
\green{"pi(x) == real(card({y. y<=x & y:prime}))"}
\green{"(%x. pi x * ln (real x) / (real x)) ----> 1"}
\end{alltt}
\end{quote}
\smallskip
\textsl{1 megabyte = 30,000 lines = 42 files of Isabelle/HOL} \\
\adviwait
\adviplay[white]{i1}%
\adviplay[slidered]{i2}%
{the \textbf{elementary} proof by Selberg from 1948}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Four Color Theorem}
Georges Gonthier:
\begin{quote}
\begin{alltt}
\green{(m : map) (simple_map m) -> (map_colorable (4) m)}
\end{alltt}
\end{quote}
\adviwait
\smallskip
\textsl{2.5 megabytes = 60,000 lines = 132 files of Coq 7.3.1} \\
streamlined proof by Robertson, Sanders, Seymour \& Thomas from 1996\toolong
\adviwait
\medskip

\begin{itemize}
\item[$\bullet$]
contains interesting mathematics as well \\
\blue{`planar hypermaps'}
\adviwait
\smallskip

\item[$\bullet$]
very interesting `own' proof language on top of Coq
\smallskip
\begingroup
\footnotesize
\begin{alltt}
\green{Move=> x' p'; Elim: p' x' => [|y' p' Hrec] x' //=; Rewrite: ~Hrec.
By Congr andb; Congr orb; Rewrite: /eqdf (monic2F_eqd (f_finv (Inode g'))).}\toolong
\end{alltt}
\endgroup
\adviwait

\item[$\bullet$]
heavily relies on \textbf{reflection} \\
\red{`this formalization really needs Coq'}

\end{itemize}

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

\begin{slide}
\slidetitle{Jordan Curve Theorem}
Tom Hales:
\begin{quote}
\begingroup
\footnotesize
\def\\{\char`\\}
\begin{alltt}
\green{`!C. simple_closed_curve top2 C ==>
   (?A B.  top2 A /\\ top2 B /\\
     connected top2 A /\\ connected top2 B /\\
   ~(A = EMPTY) /\\ ~(B = EMPTY) /\\
    (A INTER B = EMPTY) /\\ (A INTER C = EMPTY) /\\
        (B INTER C = EMPTY) /\\
       (A UNION B UNION C = euclid 2))`}
\end{alltt}
\endgroup
\end{quote}
\adviwait
\textsl{2.1 megabytes = 75,000 lines = 15 files of HOL Light} \\
proof through the Kuratowski characterization of planarity
%\adviwait
\smallskip

\begin{itemize}
\item[$\bullet$]
`warming up exercise'
for the Flyspeck project
\adviwait

\item[$\bullet$]
{beat the Mizar project at formalizing this first}
\adviwait

\item[$\bullet$]
also uses an `own' proof style

\end{itemize}

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

\begin{slide}
\sectiontitle{state of the art: current big projects}
\slidetitle{the continuous lattices formalization}
\red{formalize a complete `advanced' mathematics textbook}
\begin{quote}
\green{\textbf{A Compendium of Continuous Lattices}} \\
by Gierz, Hofmann, Keimel, Lawson, Mislove \& Scott
\end{quote}
\smallskip

\begingroup
\footnotesize
\begin{center}
\darkgray{
\setlength{\fboxsep}{.5em}
\framebox{\parbox{24em}{
\rightskip 0pt plus 1fill
\black{[\dots$\!$]}\enskip
For if not, then  $V\subseteq\bigcup\{L\setminus\mathord{\downarrow} v : v\in V\}$; and by quasicompactness and the
fact that the $L\setminus\mathord{\downarrow} v$ form a directed family, there would be a
$v\in V$ with
$V\subseteq L\setminus\mathord{\downarrow} v$, notably $v\not\in V$, which is impossible.\enskip
\black{[\dots$\!$]}
}}
}
\end{center}
\endgroup
\medskip
\adviwait
project led by Grzegorz Bancerek

\begin{center}
\green{about 70\% formalized} \\
\textsl{4.4 megabytes = 127,000 lines = 58 files of Mizar}
\end{center}
\medskip

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

\begin{slide}
\slidetitle{the Flyspeck project}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/dagen/pics/or8.eps}}
\vss
}
Kepler in \green{strena sue de nive sexangula,} 1661:

\red{is the way one customarily stacks oranges the \\
most efficient
way to stack spheres?}
\bigskip
\adviwait

Tom Hales, 1998:\quad \textbf{yes$\,$!}
\medskip
%\adviwait

proof: depends on computer checking \\
3 gigabytes programs \& data,
couple of months of computer time
\medskip
\adviwait

referees say to be \red{99\% certain} that everything is correct
\bigskip
\adviwait

\textbf{FlysPecK project} \\
\blue{`Formal Proof of Kepler'}

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

\begin{slide}
\sectiontitle{so why did the qed project not take off?}
\slidetitle{\textbf{reason one:} differences between systems}
foundations differ very much
\smallskip

\begin{center}
\green{set theory \black{$\longleftrightarrow$} type theory \black{$\longleftrightarrow$} higher order logic \black{$\longleftrightarrow$} {\small PRA}} \adviwait\\
\green{classical \black{$\longleftrightarrow$} constructive}  \adviwait\\
\green{extensional \black{$\longleftrightarrow$} intensional} \\
\green{impredicative \black{$\longleftrightarrow$} predicative} \\
\green{choice \black{$\longleftrightarrow$} only countable choice \black{$\longleftrightarrow$} no choice}
\end{center}
\medskip
\smallskip
\adviwait

\red{two utopias simultaneously?}

\begin{itemize}
\item[$\bullet$]
\textbf{formalization of mathematics}

\item[$\bullet$]
\textbf{doing mathematics in weak logics}

\end{itemize}

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

\begin{slide}
\slidetitle{\textbf{(advertisement)}\enskip a questionnaire about intuitionism}
\vspace{0pt}

\begin{center}
\blue{\url{http://www.intuitionism.org/}}
\end{center}
\adviwait
\bigskip
\medskip

\red{ten questions about intuitionism} \\
currently: seventeen sets of answers by various people
\bigskip

\begin{itemize}
\item[\green{3.}]
\green{Do you agree that there are only three infinite cardinalities?}

\item[\green{7.}]
\green{Do you agree that for any two statements the first
implies the second or the second implies the first?}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{putting systems together}
\slidetitle{OMDoc}
\green{XML standard for encoding of mathematical documents} \\
developed by Michael Kohlhase
\medskip

can be used both for natural language documents and for formalizations \\
modularized language architecture
\adviwait
\medskip

supports both \blue{OpenMath} and \blue{Content MathML} encoding of formulas
\adviwait
\medskip

\red{does not really address semantical differences between systems}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Logosphere}
\green{converting between the foundations of various systems} \\
project led by Carsten Sch\"urmann
\medskip

\red{formalize foundations of each system in the Twelf logical framework} \\
translate all formalizations into Twelf \\
use Twelf to relate those formalizations
\medskip
\adviwait

systems that are currently supported:
\begin{itemize}
\item[$\bullet$]
\textbf{first order resolution provers}
\item[$\bullet$]
\textbf{HOL}
\item[$\bullet$]
\textbf{NuPRL}
\item[$\bullet$]
\textbf{PVS}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{reason two: {\sf why mathematicians are not interested (yet)}}
\slidetitle{the cost is too high\dots}
$$\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 the gain is too little}
\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 we just have 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{and it does not look like mathematics}
\adviwait
most systems: \green{`proof' = list of tactics} = \red{unreadable computer code} \\\adviwait
{even in Mizar and Isar}: \textbf{still} looks like code
\adviwait
\bigskip

\green{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)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{so what is needed most to promote formalization of mathematics?}
\begin{itemize}
%\item[$\bullet$] proof search: not very powerful, not very important
\item[$\bullet$] \textbf{decision procedures} \\
very important, main strength of PVS\adviwait
\medskip

\item[$\bullet$]
in particular: \textbf{computer algebra} \\
\green{Macsyma, Maple, Mathematica} \\
(really: \textbf{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}

\begin{slide}
\slidetitle{\Large second hour: \\
\red{a tour of Mizar}, a proof assistant for mathematics}
\end{slide}

\begin{slide}
\slidetitle{why is Mizar interesting?}
\begin{itemize}
\item[$\bullet$]
\textbf{a system for mathematicians}
\adviwait

\item[$\bullet$]
\textbf{the proof language}

only other system with similar language: \green{Isabelle/Isar}
\adviwait

\item[$\bullet$]
\textbf{\red{many other interesting ideas}}

\begin{itemize}
\item
type system

\begin{itemize}
\item[]
soft typing

\item[]
`attributes'

\item[]
multiple inheritance between structure types

\end{itemize}

\item
expression syntax

\begin{itemize}
\item[]
type directed overloading

\item[]
bracket-like operators

\item[]
arbitrary {\small ASCII} strings for operators

\end{itemize}

\end{itemize}

\end{itemize}

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

\begin{slide}
\sectiontitle{example formalizations}
\slidetitle{example: Coq version}
\vspace{-1.8\bigskipamount}
\begingroup
\def\xto{$\to$}
\def\xleftarrow{$\leftarrow$}
\begin{alltt}
\red{Definition} ge (n m : \blue{nat}) : Prop :=
  exists x : \blue{nat}, n = m + x.
\red{Infix} ">=" := \blue{ge} : nat_scope.\medskip\adviwait
\red{Lemma} ge_trans :
  forall n m p : \blue{nat}, n >= m -> m >= p -> n >= p.\adviwait
\red{Proof}.
 unfold ge. intros n m p H H0.
 elim H. clear H. intros x H1.
 elim H0. clear H0. intros x0 H2.
 exists (x0 + x).
 rewrite \blue{plus_assoc}. rewrite <- H2. auto.
\red{Qed}.
\end{alltt}
\endgroup

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

\begin{slide}
\slidetitle{example: Mizar version}
\vspace{-1.8\bigskipamount}
\begin{alltt}
\red{reserve} n,m,p,x,x0 for natural number;\medskip
\red{definition} let n,m;
 pred n >= m means :ge: ex x st n = m \blue{+} x;
\red{end};\medskip
\red{theorem} ge_trans: n \blue{>=} m & m \blue{>=} p implies n \blue{>=} p
\red{proof}\adviwait
 \green{assume that H: n \blue{>=} m and H0: m \blue{>=} p;\adviwait
 consider x such that H1: n = m \blue{+} x by H,ge;\adviwait
 consider x0 such that H2: m = p \blue{+} x0 by H0,ge;\adviwait
 n = p \blue{+} (x \blue{+} x0) by H1,H2;\adviwait
 hence n \blue{>=} p by ge;}\adviwait
\red{end};
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural versus declarative}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\green{
\begin{picture}(5,5)
\advirecord{e0}{
\put(0,5){\line(1,0){5}}
\put(.5,4.5){\makebox(0,0){\black{\scriptsize $0$}}}
\put(0,4){\line(1,0){3}}
\put(1,3){\line(1,0){2}}
\put(2,2){\line(1,0){1}}
\put(4,2){\line(1,0){1}}
\put(3,1){\line(1,0){2}}
\put(4.5,.5){\makebox(0,0){\black{\scriptsize $\infty$}}}
\put(0,0){\line(1,0){5}}
\put(0,0){\line(0,1){5}}
\put(1,1){\line(0,1){2}}
\put(2,0){\line(0,1){1}}
\put(3,1){\line(0,1){2}}
\put(4,2){\line(0,1){2}}
\put(5,0){\line(0,1){5}}
}
\adviplay[slidegreen]{e0}
\put(0.2,4.5){\makebox(0,0){\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,4.5){\makebox(0,0){\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,4.5){\makebox(0,0){\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,4.5){\makebox(0,0){\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,3.5){\makebox(0,0){\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,3.5){\makebox(0,0){\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,3.5){\makebox(0,0){\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,3.5){\makebox(0,0){\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,2.5){\makebox(0,0){\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,1.5){\makebox(0,0){\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,0.5){\makebox(0,0){\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,0.5){\makebox(0,0){\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,1.5){\makebox(0,0){\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,1.5){\makebox(0,0){\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,0.5){\makebox(0,0){\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,0.5){\makebox(0,0){\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}
\put(4.2,0.5){\makebox(0,0){\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}
\end{picture}
}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%

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

\begingroup
\small
\green{%
\adviwait
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
E
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
E
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
S
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
E
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
N
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
E
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
S
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
S
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
S
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
W
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
W
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
W
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
S
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
E
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
E
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
E
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidegreen]{e0}
}
\endgroup

HOL, \blue{Isabelle}, \blue{Coq}, NuPRL, PVS

\adviwait
\item[$\bullet$]
\textbf{declarative}

\begingroup
\scriptsize
\green{
\adviwait
(0,0)
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
(1,0)
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
(2,0)
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
(3,0)
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
(3,1)
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
(2,1)
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
(1,1)
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
(0,1)
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
(0,2)
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
(0,3)
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
(0,4)
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
(1,4)
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
(1,3)
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
(2,3)
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
(2,4)
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
(3,4)
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
(4,4)
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%
}\toolong
\endgroup

\red{Mizar}, \blue{Isabelle}

\end{itemize}

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

\begin{slide}
\slidetitle{another small example}
\vspace{-\medskipamount}
\begin{center}
{
\setlength{\fboxsep}{.5em}
\framebox{\parbox{24em}{
\textsl{If every poor person has a rich father, \\
then there is a rich person with a rich grandfather.}
}}
}
\end{center}
\bigskip
\adviwait

\begin{alltt}
 assume that
A1: for x st x is poor holds father(x) is rich and
A2: not ex x st x is rich & father(father(x)) is rich;\adviwait
 consider p being person;\adviwait
 now let x;
  x is poor or father(father(x)) is poor by A2;
  hence father(x) is rich by A1;
 end;\adviwait
 then father(p) is rich & father(father(father(p))) is rich;\toolong
 hence contradiction by A2;
\end{alltt}

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

\begin{slide}
\slidetitle{demo example}


\textbf{Theorem. }%
\textsl{There are irrational numbers \red{$x$} and \red{$y$}
such that \green{$x^y$} is rational.\adviwait}

\textbf{Proof. }%
We have the following calculation
$${\big(\sqrt{2}^{\sqrt{2}}\rlap{$\big)$}{\scriptscriptstyle\strut}}^{\sqrt{2}}
=
\sqrt{2}^{\sqrt{2}\cdot\sqrt{2}} =
\sqrt{2}^{\,2} =
\green{2}$$
which is rational.
%\adviwait
Furthermore Pythagoras showed that \red{$\sqrt{2}$} is irrational.
\adviwait
Now there are two cases:
\begin{itemize}
\item[$\bullet$]
Either \green{$\sqrt{2}^{\sqrt{2}}$} is rational.
\advirecord{f1}{Then take $\red{x = y = \sqrt{2}}$.}

\item[$\bullet$]
Or $\red{\sqrt{2}^{\sqrt{2}}}$ is irrational.
\advirecord{f2}{In that case take \red{$x = \sqrt{2}^{\sqrt{2}}$} and \red{$y =
\sqrt{2}$}.
And by the above calculation then \green{$x^y = 2$}, which is rational.
\hfill$\Box$}

\end{itemize}
\adviwait
\adviplay{f1}
\adviwait
\adviplay{f2}
%\adviwait
%(Note that the proof doesn't say which of the two cases holds!)

%\vspace{-11pt}
\vfill
\end{slide}

\def\Implies{\,\Rightarrow\,}
\def\Iff{\,\Leftrightarrow\,}

\begin{slide}
\slidetitle{lemmas used in the proof}

\def\_{\char`\_}
\def\^{\char`\^}

\begin{center}
\begin{tabular}{lcc}
\texttt{AXIOMS:22} &$\qquad$& $x \le y \,\land\, y \le z \Implies x \le z$ \\
\texttt{INT\_2:44} && $2\mbox{ is prime}$ \\
\texttt{IRRAT\_1:1} && $p\mbox{ is prime} \Implies \sqrt{p} \,\not\in {\mathbb Q}$ \\
\texttt{POWER:38} && $a > 0 \Implies {(a^b)}^c = a^{bc}$ \\
\texttt{SQUARE\_1:def 3} && $\red{x^2} = x \cdot x$ \\
\texttt{SQUARE\_1:def 4} && $0 \le a \Implies (x = \red{\sqrt{a}} \Iff 0 \le x \,\land\, x^2 = a)$ \\
\texttt{SQUARE\_1:84} && $1 < \sqrt{2}$ \\
\noalign{\adviwait}
\texttt{POWER:53} && `$\,$\texttt{a to\_power 2 = a\^2}$\,$'
\end{tabular}$\hspace{-1em}$
\end{center}
\adviwait
\bigskip

\begin{center}
\large
\gray{DEMO}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example of how Mizar is like English}
Hardy \& Wright, \green{An Introduction to the Theory of Numbers}%: \textbf{7 lines}
%\adviwait
\medskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}
\begin{center}
\setlength{\fboxsep}{.5em}
$\hspace{-2em}$\framebox{\hspace{.1em}\parbox{\linewidth}{
\textbf{Theorem 43 (Pythagoras' theorem).} {$\sqrt{2}$ is irrational.}
\medskip

\rightskip=0pt
The traditional proof ascribed to Pythagoras runs
as follows.  If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{\textsf{(4.3.1)}}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$.  Hence $a^2$ is even, and there%-
fore $a$ is even.  If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$.
\hfill$\Box$%
\smallskip
}\hspace{.3em}}$\hspace{-2em}$
\end{center}
\end{quote}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar language approximation of this text}
\vspace{-1.5\medskipamount}

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}\small
\advirecord{a1}{\textbf{theorem} Th43: sqrt 2 is irrational} \\
%$\,$:: \textbf{Pythagoras' theorem}}$\hspace{-1em}$ \\
\advirecord{a2}{\textbf{proof}} \\
\advirecord{a3}{\quadskip \textbf{assume} sqrt 2 is rational\textbf{;}} \\
\advirecord{a4}{\quadskip \textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}} \\
\advirecord{a5}{4\_3\_1: a\char`^2 = 2$\,*\,$b\char`^2 \textbf{and}} \\
\advirecord{a6}{\quadskip\quadskip a,b are\_relative\_prime\textbf{;}} \\
\advirecord{a7}{\quadskip a\char`^2 is even\textbf{;}} \\
\advirecord{a8}{\quadskip a is even\textbf{;}} \\
\advirecord{a9}{\quadskip \textbf{consider} c \textbf{such that} a = 2$\,*\,$c\textbf{;}} \\
\advirecord{a10}{\quadskip 4$\,*\,$c\char`^2 = 2$\,*\,$b\char`^2\textbf{;}} \\
\advirecord{a11}{\quadskip 2$\,*\,$c\char`^2 = b\char`^2\textbf{;}} \\
\advirecord{a12}{\quadskip b is even\textbf{;}} \\
\advirecord{a13}{\quadskip \textbf{thus} contradiction\textbf{;}} \\
\advirecord{a14}{\textbf{end;}}
\end{quote}
\adviplay{a1}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviplay{a5}
\adviplay{a6}
\adviplay{a7}
\adviplay{a8}
\adviplay{a9}
\adviplay{a10}
\adviplay{a11}
\adviplay{a12}
\adviplay{a13}
\adviplay{a14}
\vss
}
\adviwait
\vbox to 0pt{
\vspace{-2.2\bigskipamount}
\begin{quote}
\rightskip=0pt
\advirecord{b1}{\textbf{theorem} Th43: {sqrt 2 is irrational} $\,$:: \textbf{Pythagoras' theorem}}
\medskip

\advirecord{b2}{\textbf{proof}$\,$} \advirecord{b3}{assume sqrt 2
is rational;} \advirecord{b4}{consider $a,b$ such that}
\advirecord{b5}{$$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$
and} \advirecord{b6}{$a,b$ are\_relative\_prime;} \advirecord{b7}{$a\mathbin{\hat{}}2$ is even;}
\advirecord{b8}{$a$ is even;} \advirecord{b9}{consider $c$ such that $a = 2\mathbin{*}c$;} \advirecord{b10}{$4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$;} \advirecord{b11}{$2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$;} \advirecord{b12}{$b$ is
even;} \advirecord{b13}{thus contradiction;} \hfill \advirecord{b14}{end;}
\end{quote}
\adviplay[white]{a1}\adviplay{b1}\adviwait[.8]
\adviplay[white]{a2}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a3}\adviplay{b3}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a4}\adviplay{b4}\adviwait[.8]
\adviplay[white]{a5}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a6}\adviplay{b6}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a7}\adviplay{b7}\adviwait[.8]
\adviplay[white]{a8}\adviplay{b8}\adviwait[.8]
\adviplay[white]{a9}\adviplay{b9}\adviwait[.8]
\adviplay[white]{a10}\adviplay{b10}\adviwait[.8]
\adviplay[white]{a11}\adviplay{b11}\adviwait[.8]
\adviplay[white]{a12}\adviplay{b12}\adviwait[.8]
\adviplay[white]{a13}\adviplay{b13}\adviwait[.8]
\adviplay[white]{a14}\adviplay{b14}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{full Mizar}
\vspace{-2\medskipamount}

\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c1}{\textbf{theorem} Th43: sqrt 2 is irrational}\\
\advirecord{c2}{\textbf{proof}}\\
\advirecord{c3}{\quad \textbf{assume} sqrt 2 is rational\textbf{;}}\\
\advirecord{c4}{\quad \textbf{then} }\advirecord{c5}{\textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}}\\
\advirecord{c6a}{A1: }\advirecord{c6b}{b {\tiny \raise.8pt\hbox{$<>$}} 0 \textbf{and}}\\
\advirecord{c7a}{A2: }\advirecord{c7b}{sqrt 2 = a/b \textbf{and}}\\
\advirecord{c8}{A3: }\advirecord{c9}{a,{\tiny $\,$}b are\_relative\_prime}\advirecord{c10a}{ \textbf{by} Def1}\advirecord{c10b}{\textbf{;}}\\
\advirecord{c11a}{A4: }\advirecord{c11b}{b\^{}2 {\tiny \raise.8pt\hbox{$<>$}} 0}\advirecord{c11c}{ \textbf{by} A1,{\tiny $\,$}{\tiny SQUARE\_}1:73}\advirecord{c11d}{\textbf{;}}\\
\advirecord{c12a}{\quad 2 = (a/b)\^{}2}\advirecord{c12b}{ \textbf{by} A2,{\tiny
$\,$}{\tiny SQUARE\_}1:def 4}\\
\advirecord{c13a}{\qquad .= a\^{}2/b\^{}2}\advirecord{c13b}{ \textbf{by} {\tiny
SQUARE\_}1:69}\advirecord{c13c}{\textbf{;}}\\
\advirecord{c14}{\quad \textbf{then}}\\
\advirecord{c15}{4\_3\_1: a\^{}2 = 2$\,*\,$b\^{}2}\advirecord{c16}{ \textbf{by}
A4,{\tiny $\,$}{\tiny REAL\_}1:43}\advirecord{c17}{\textbf{;}}\\
\advirecord{c18}{\quad a\^{}2 is even}\advirecord{c19}{ \textbf{by} 4\_3\_1,{\tiny $\,$}{\tiny ABIAN}:def 1}\advirecord{c20}{\textbf{;}}\\
\advirecord{c21}{\quad \textbf{then}}\\
\advirecord{c22}{A5: }\advirecord{c23}{a is even}\advirecord{c24}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c25}{\textbf{;}}\\
\green{:: \textbf{continue in next column}}
\end{flushleft}
}\hfill\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c26}{\quad \textbf{then} }\advirecord{c27}{\textbf{consider} c \textbf{such that}} \\
\advirecord{c28}{A6: }\advirecord{c29}{a = 2$\,*\,$c}\advirecord{c30}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c31}{\textbf{;}} \\
\advirecord{c32}{A7: }\advirecord{c33}{4$\,*\,$c\^{}2 =}\advirecord{c34}{ (2$\,*\,$2)$\,*\,$c\^{}2}\\
\advirecord{c35a}{\qquad .= 2\^{}2$\,*\,$c\^{}2}\advirecord{c35b}{ \textbf{by} {\tiny SQUARE\_}1:def 3}\\
\advirecord{c36}{\qquad .= }\advirecord{c37}{2$\,*\,$b\^{}2}\advirecord{c38}{ \textbf{by} A6,{\tiny $\,$}4\_3\_1,{\tiny $\,$}{\tiny SQUARE\_}1:68}\advirecord{c39}{\textbf{;}}\\
\advirecord{c40a}{\quad 2$\,*\,$(2$\,*\,$c\^{}2) = (2$\,*\,$2)$\,*\,$c\^{}2}\advirecord{c40b}{ \textbf{by} {\tiny AXIOMS}:16}\\
\advirecord{c41a}{\qquad .= 2$\,*\,$b\^{}2}\advirecord{c41b}{ \textbf{by} A7}\advirecord{c41c}{\textbf{;}}\\
\advirecord{c42}{\quad \textbf{then} }\advirecord{c43}{2$\,*\,$c\^{}2 = b\^{}2}\advirecord{c44}{ \textbf{by} {\tiny REAL\_}1:9}\advirecord{c45}{\textbf{;}}\\
\advirecord{c46a}{\quad \textbf{then} }\advirecord{c46b}{b\^{}2 is even}\advirecord{c46c}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c46d}{\textbf{;}}\\
\advirecord{c47}{\quad \textbf{then} }\advirecord{c48}{b is even}\advirecord{c49}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c50}{\textbf{;}}\\
\advirecord{c51a}{\quad \textbf{then} }\advirecord{c51b}{2 divides a \& 2 divides b}\advirecord{c51c}{ \textbf{by} A5,{\tiny $\,$}Def2}\advirecord{c51d}{\textbf{;}}\\
\advirecord{c52}{\quad \textbf{then}}\\
\advirecord{c53a}{A8: }\advirecord{c53b}{2 divides a gcd b}\advirecord{c53c}{ \textbf{by} {\tiny INT\_}2:33}\advirecord{c53d}{\textbf{;}}\\
\advirecord{c54a}{\quad a gcd b = 1}\advirecord{c54b}{ \textbf{by} A3,{\tiny $\,$}{\tiny INT\_}2:def 4}\advirecord{c54c}{\textbf{;}}\\
\advirecord{c55}{\quad \textbf{hence} contradiction}\advirecord{c56}{ \textbf{by} A8,{\tiny $\,$}{\tiny INT\_}2:17}\advirecord{c57}{\textbf{;}}\\
\advirecord{c58}{\textbf{end;}}
\end{flushleft}
}
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay{c5}
\adviplay{c9}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c23}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviplay{c33}
\adviplay{c37}
\adviplay{c39}
\adviplay{c43}
\adviplay{c45}
\adviplay{c48}
\adviplay{c50}
\adviplay{c55}
\adviplay{c57}
\adviplay{c58}
\adviwait
\adviplay[slideblue]{c6b}
\adviplay[slideblue]{c7b}
\adviplay[slideblue]{c10b}
\adviplay[slideblue]{c11b}
\adviplay[slideblue]{c11d}
\adviplay[slideblue]{c12a}
\adviplay[slideblue]{c13a}
\adviplay[slideblue]{c13c}
\adviplay[slideblue]{c34}
\adviplay[slideblue]{c35a}
\adviplay[slideblue]{c36}
\adviplay[slideblue]{c40a}
\adviplay[slideblue]{c41a}
\adviplay[slideblue]{c41c}
\adviplay[slideblue]{c46b}
\adviplay[slideblue]{c46d}
\adviplay[slideblue]{c51b}
\adviplay[slideblue]{c51d}
\adviplay[slideblue]{c53b}
\adviplay[slideblue]{c53d}
\adviplay[slideblue]{c54a}
\adviplay[slideblue]{c54c}
\adviwait
\adviplay[slidered]{c4}
\adviplay[slidered]{c14}
\adviplay[slidered]{c21}
\adviplay[slidered]{c26}
\adviplay[slidered]{c42}
\adviplay[slidered]{c46a}
\adviplay[slidered]{c47}
\adviplay[slidered]{c51a}
\adviplay[slidered]{c52}
\adviwait
\adviplay[slidered]{c6a}
\adviplay[slidered]{c7a}
\adviplay[slidered]{c8}
\adviplay[slidered]{c11a}
\adviplay[slidered]{c22}
\adviplay[slidered]{c28}
\adviplay[slidered]{c32}
\adviplay[slidered]{c53a}
\adviwait
\adviplay[slidered]{c10a}
\adviplay[slidered]{c11c}
\adviplay[slidered]{c12b}
\adviplay[slidered]{c13b}
\adviplay[slidered]{c16}
\adviplay[slidered]{c19}
\adviplay[slidered]{c24}
\adviplay[slidered]{c30}
\adviplay[slidered]{c35b}
\adviplay[slidered]{c38}
\adviplay[slidered]{c40b}
\adviplay[slidered]{c41b}
\adviplay[slidered]{c44}
\adviplay[slidered]{c46c}
\adviplay[slidered]{c49}
\adviplay[slidered]{c51c}
\adviplay[slidered]{c53c}
\adviplay[slidered]{c54b}
\adviplay[slidered]{c56}
\adviwait
\adviplay{c6b}
\adviplay{c7b}
\adviplay{c10b}
\adviplay{c11b}
\adviplay{c11d}
\adviplay{c12a}
\adviplay{c13a}
\adviplay{c13c}
\adviplay{c34}
\adviplay{c35a}
\adviplay{c36}
\adviplay{c40a}
\adviplay{c41a}
\adviplay{c41c}
\adviplay{c46b}
\adviplay{c46d}
\adviplay{c51b}
\adviplay{c51d}
\adviplay{c53b}
\adviplay{c53d}
\adviplay{c54a}
\adviplay{c54c}
\adviplay{c4}
\adviplay{c14}
\adviplay{c21}
\adviplay{c26}
\adviplay{c42}
\adviplay{c46a}
\adviplay{c47}
\adviplay{c51a}
\adviplay{c52}
\adviplay{c6a}
\adviplay{c7a}
\adviplay{c8}
\adviplay{c11a}
\adviplay{c22}
\adviplay{c28}
\adviplay{c32}
\adviplay{c53a}
\adviplay{c10a}
\adviplay{c11c}
\adviplay{c12b}
\adviplay{c13b}
\adviplay{c16}
\adviplay{c19}
\adviplay{c24}
\adviplay{c30}
\adviplay{c35b}
\adviplay{c38}
\adviplay{c40b}
\adviplay{c41b}
\adviplay{c44}
\adviplay{c46c}
\adviplay{c49}
\adviplay{c51c}
\adviplay{c53c}
\adviplay{c54b}
\adviplay{c56}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{some explanations about Mizar}
\slidetitle{the proof language}
\red{forward reasoning}

\begin{tabular}{l}
\notion{statement} \textbf{by} \notion{references} \vspace{-\smallskipamount}\adviwait\\
\notion{statement} \textbf{proof} \notion{steps} \textbf{end}
\end{tabular}
\adviwait

\red{natural deduction}

\begin{tabular}{lcl}
 \textbf{thus} \notion{statement} &$\green{\to}$& closes the proof \vspace{-\smallskipamount}\adviwait\\
\textbf{assume} \notion{statement} &$\green{\to}$& $\to$-introduction \vspace{-\smallskipamount}\adviwait\\
\textbf{let} \notion{variable} &$\green{\to}$& $\forall$-introduction \vspace{-\smallskipamount}\\
\textbf{thus} \notion{statement}  &$\green{\to}$& $\land$-introduction \vspace{-\smallskipamount}\\
\textbf{consider} \notion{variable} \textbf{such that} \notion{statement} &$\green{\to}$& $\exists$-elimination \vspace{-\smallskipamount}\\
\textbf{take} \notion{term} &$\green{\to}$& $\exists$-introduction \vspace{-\smallskipamount}\adviwait\\
\textbf{per} \textbf{cases;}\enskip \textbf{suppose} \notion{statement}\textbf{;}\enskip \dots &$\green{\to}$& $\lor$-elimination
\end{tabular}\toolong

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

\begin{slide}
\slidetitle{`semantics'?}
Mizar is just \red{first order predicate logic + set theory} \adviwait\\
Mizar proofs are just \green{Fitch-style natural deduction} \adviwait

\textbf{but:}
\begin{itemize}
\item[$\bullet$]
Mizar variables have types\dots\\
{\dots} and these types are quite powerful!

\item[$\bullet$]
Mizar has `second-order theorems' called \blue{schemes}

\item[$\bullet$]
Mizar defines function symbols using something like Church's \\ $\iota$ operator
(`unique choice')

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Tarski-Grothendieck set theory}
\vbox to 0pt{
\vspace{-1.5\bigskipamount}
\begin{center}
\footnotesize
\begin{tabular}{lcc}
\texttt{TARSKI:def 3} && $\red{X \subseteq Y} \Iff (\forall x.\; x \in X \Implies x \in Y)$ \\
\texttt{TARSKI:def 5} && $\red{\langle x,y\rangle} = \{\{x,y\},\{x\}\}$ \\
\texttt{TARSKI:def 6} && $\red{X \sim Y} \Iff \exists Z.\, (\forall x.\, x \in X. \!\Implies\! \exists y.\, y \in Y \land \langle x,y\rangle \in Z) \land {}$ \\&& $\phantom{X \sim Y \Iff \exists Z.\,} (\forall y.\, y \in Y. \!\Implies\! \exists x.\, x \in X \land \langle x,y\rangle \in Z) \land {}$ \\
&& $(\forall x \forall y \forall z \forall u.\, \langle x,y\rangle \in Z \land \langle z,u\rangle \in Z \Implies (x = z \Iff y = u))$ \\
\noalign{\vspace{-.1em}\color{slideblue}\rule{\linewidth}{0.04em}\vspace{.2em}}%
\texttt{TARSKI:def 1} && $x \in \red{\{y\}} \Iff x = y$ \\
\texttt{TARSKI:def 2} && $x \in \red{\{y,z\}} \Iff x = y \,\lor\, x = z$ \\
\texttt{TARSKI:def 4} && $x \in \red{\bigcup X} \Iff \exists Y.\; x \in Y \,\land\, Y \in X$ \\
\noalign{\medskip}
\texttt{TARSKI:2} && $(\forall x.\; x\in X \!\Iff\! x\in Y) \Implies X = Y$ \\
\texttt{TARSKI:7} && $x \in X \Implies \exists Y.\; Y \in X \land \neg\exists x.\; x \in X \land x \in Y$ \\
\green{\texttt{TARSKI:sch 1}} && \green{$(\forall x\,\forall y\,\forall z.\, P[x,y] \land P[x,z] \!\Implies\! y = z) \rlap{${} \Implies {}$}$} \\
&& \green{$(\exists X.\; \forall x.\; x \in X \Iff \exists y.\; y \in A \,\land\, P[y,x])$} \\
\texttt{TARSKI:9} && $\exists M.\, N\in M \land (\forall X\forall Y.\, X \in M \land Y \subseteq X \!\Implies\! Y \in M) \land {}$ \\
&& $(\forall X.\, X \in M \!\Implies\! \exists Z.\, Z \in M \land \forall Y.\, Y \subseteq X \!\Implies\! Y \in Z) \land {}$ \\
&& $(\forall X.\, X \subseteq M \!\Implies\! X \sim M \lor X \in M)$
\end{tabular}
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{types!}
Mizar is based on set theory but it is a \red{typed} system
\adviwait

Mizar types are \red{soft} types:
$$M : N(t_1,\dots,t_n)$$
should really be read as a \textbf{predicate}
$$N(t_1,\dots,t_n,M)\adviwait$$

This means that:
\begin{itemize}
\item[$\bullet$]
one Mizar term can have many different types at the same time

\item[$\bullet$]
a Mizar typing can be used as a logical formula!
$$
\mbox{\texttt{let \green{x be Real};}}
\qquad\longleftrightarrow\qquad
\mbox{\texttt{assume not \green{x is Nat};}}
$$

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{types! (continued)}
\green{think of Mizar types as predicates that the system keeps track of for you}\toolong
\adviwait

Mizar types are used for three things:
\begin{itemize}
\item[$\bullet$]
\textbf{type based overloading}
\begin{tabular}{ll}
\texttt{x + y}\quad & sum of two numbers \vspace{-\smallskipamount}\adviwait\\
\texttt{X + Y} & adding the elements of two sets \vspace{-\smallskipamount}\adviwait\\
\texttt{X + y} & mixing these two things \vspace{-\smallskipamount}\adviwait\\
\texttt{v + w} & sum of two elements of a vector space \vspace{-\smallskipamount}\adviwait\\
%\texttt{p + q} & sum of two polynomials \vspace{-\smallskipamount}\adviwait\\
\texttt{I + J} & sum of two ideals in a ring \vspace{-\smallskipamount}\adviwait\\
\texttt{x + y} & `join' of two elements of a lattice \vspace{-\smallskipamount}\adviwait\\
\texttt{p + i} & adding an offset to a pointer\adviwait
\end{tabular}

\item[$\bullet$]
\textbf{inferring implicit arguments}
\adviwait

\item[$\bullet$]
\textbf{automatic inference of propositions}

\end{itemize}

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

\begin{slide}
\slidetitle{types! (continued)}
\begin{itemize}
\item[$\bullet$]
Mizar has \red{dependent} types \\
(much like in all the other dependent type systems)
\adviwait

\item[$\bullet$]
Mizar has a \red{subtype} relation \\
every type except the type `\texttt{set}' has a supertype
\adviwait

\item[$\bullet$]
Mizar has `type modifiers' called \red{attributes} \\
a type can be prefixed with one or more \red{adjectives} \\
an adjective is either an attribute or the negation of an attribute \\
(behaves like \green{intersection types})

\end{itemize}
\bigskip

\begin{center}
{\tt \framebox{\tt \framebox{\tt non empty\strut} \framebox{\tt finite\strut}} \framebox{\tt \underline{\tt Subset} of NAT\strut}}
\end{center}

\vfill
\end{slide}

\if 0
\begin{slide}
\slidetitle{types! (continued)}
\begin{itemize}
\item[$\bullet$]
Mizar has \red{structure} types \\
(Mizar's structure types support multiple inheritance)

\item[$\bullet$]
Mizar uses its dependent types to support \red{implicit arguments}

\end{itemize}

Mizar's structure types together with the attributes and the implicit arguments
give a powerful framework for doing abstract mathematics

\vfill
\end{slide}
\fi

\begin{slide}
\slidetitle{notation}
\textbf{any} {\small ASCII} string can be used for a Mizar operator
\medskip

\begingroup
\small
\begin{quote}
\begin{alltt}
  func \red{].}a,b\red{.]} -> Subset of REAL means
\green{:: MEASURE5:def 3}
   for x being \red{R_eal} holds
    x in it iff (a \red{<'} x & x \red{<='} b & x in \red{REAL});
\end{alltt}
\end{quote}
\smallskip

\begin{quote}
\begin{alltt}
  pred a,b \red{are_convergent<=1_wrt} R means
\green{:: REWRITE1:def 9}
   ex c being set st (\red{[}a,c\red{]} in R or a = c) & (\red{[}b,c\red{]} in R or b = c);\toolong
\end{alltt}
\end{quote}
\endgroup

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar in the world}
\slidetitle{Mizar Mathematical Library}

\green{the biggest library of formalized mathematics}
\medskip
\adviwait

\begin{center}
\begin{tabular}{rl}
\red{49,588} & \red{lemmas} \\
1,820,879 & lines of `code' \\
64 & megabytes \\
\noalign{\medskip}
\red{165} & \red{`authors'} \\
912 & `articles'
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar, the program}
\begin{itemize}
\item[$\bullet$]
implemented in Delphi Pascal/Free Pascal

\item[$\bullet$]
source \red{not} freely available\adviwait, but
\medskip
\begin{center}
\green{write Mizar `article' \\
$\downarrow$ \\
become member of Association of Mizar Users \\
$\downarrow$ \\
get source}
\end{center}
\medskip
\adviwait

\item[$\bullet$]
no small proof checking `kernel' \\
correctness of Mizar check depends on correctness of whole program
\adviwait

\item[$\bullet$]
users can not automate proofs inside the system

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{publishing formalizations: MML and FM}
\vspace{-1.2\bigskipamount}

\textbf{Mizar Mathematical Library}
\begin{quote}
\begingroup
\small
\begin{alltt}
\red{theorem} \green{::{\small RUSUB_2:35}}
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Compl of W holds
  V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;\toolong
\end{alltt}
\endgroup
\end{quote}
\medskip
\adviwait

\textbf{Formalized Mathematics}
\medskip
\begin{center}
{
\setlength{\fboxsep}{.5em}
\framebox{\parbox{26em}{
\rightskip 0pt plus 1fill
(35)\quad Let $V$ be a real unitary space, $W$ be a subspace of $V$, \\{\tiny\strut}$\quad$ and $L$ be a linear
complement of $W$.  Then $V$ is the direct \\{\tiny\strut}$\quad$ sum of $L$ and $W$ and the direct
sum of $W$ and $L$.
}}
}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar versus Isar}
\textbf{\adviwait some reasons to prefer Mizar over Isar}
\begin{itemize}
\item[$\bullet$]
the set theory of Mizar is much \red{more powerful and expressive} than the HOL logic of Isabelle/HOL

\item[$\bullet$]
Mizar is much more able to talk about \red{abstract mathematics}, and in particular about algebraic structures, with nice notation

\item[$\bullet$]
\red{dependent types} are way cool

\end{itemize}
\adviwait

\textbf{some reasons to prefer Isar over Mizar}
\begin{itemize}
\item[$\bullet$]
Isabelle gives you an \red{interactive} system

\item[$\bullet$]
Isabelle allows you to \red{mix} declarative and procedural proof

\item[$\bullet$]
Isabelle has much more possibilities of \red{automation}

\item[$\bullet$]
Isabelle allows you to define \red{binders}

\end{itemize}

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

\begin{slide}
\slidetitle{is Mizar a difficult system?}
\vspace{0pt}
\begin{center}
\adviwait
\textbf{{no}, not difficult at all!}
\end{center}
\bigskip

\red{Mizar is about as complex as the Pascal programming language} \\
(proof assistants tend to resemble their implementation language)
\adviwait
\bigskip

\green{reasons that people sometimes think Mizar is a complex language}
\begin{itemize}
\item[$\bullet$]
lack of proper documentation

\item[$\bullet$]
natural language-like syntax

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{extro}
\slidetitle{gazing into the crystal ball}
\green{Henk's futuristic {\qed} questions}
\medskip
\begin{itemize}
\item[$\bullet$]
will proof assistants \red{ever} become common among mathematicians?

\item[$\bullet$]
if so: \red{when} will this happen?
\medskip
\adviwait

\begin{itemize}
\item
\green{the most optimistic answer: it already is here!}

\item
\green{the experienced user's answer: {fifty years}}

\end{itemize}
\end{itemize}
\bigskip

\red{but what do \textbf{you} expect?}

\vfill
\end{slide}

\end{document}