\def\pics{cursus-pics}
\def\pics{/home/freek/talks/cursus/cursus-pics}

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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\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{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut de kunst van het bewijzen}

\red{Freek Wiedijk} \& \red{Herman Geuvers} \\
Radboud Universiteit Nijmegen \& Technische Universiteit Eindhoven
\medskip

\blue{Vakantiecursus wiskunde 2008}

\green{Technische Universiteit Eindhoven} \\
{2008\hspace{3pt}08\hspace{3pt}23, 14\hspace{1pt}:\hspace{1.8pt}15}

\green{Centrum voor Wiskunde en Informatica, Amsterdam} \\
{2008\hspace{3pt}08\hspace{3pt}29, 18\hspace{1pt}:\hspace{1.8pt}30}

\end{slide}

\begin{slide}
\sectiontitle{lagere en hogere wiskunde}
\slidetitle{de twee soorten wiskunde}
\begin{itemize}
\item[$\bullet$]
\textbf{berekenen}

\green{bij berekenen gaat het om \textsl{de uitkomst}}
\medskip

\red{\textbf{wat?}}

\bigskip
\item[$\bullet$]
\textbf{bewijzen}

\green{bij bewijzen gaat het om \textsl{het begrip}}
\medskip

\red{\textbf{waarom?}}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{het diagonaal van een vierkant}
\begin{center}
\bigskip
\vspace{-\smallskipamount}
\begin{picture}(63,63)(0,0)
\thinlines
\advirecord{a23}{\put(0,0){{\line(1,0){63}}}}%
\advirecord{a24}{\put(0,63){{\line(1,0){63}}}}%
\advirecord{a25}{\put(63,0){{\line(0,1){63}}}}%
\advirecord{a1}{\put(0,63){{\line(1,-1){63}}}}%
\advirecord{a2}{\put(0,0){{\line(0,1){63}}}}%
\thicklines
\green{\advirecord{a3}{\put(0,63){\line(1,-1){63}}}}%
\green{\advirecord{a4}{\put(0,0){\line(0,1){63}}}}%
\red{\advirecord{a5}{\put(0,0.2){\circle*{3}}}}%
\red{\advirecord{a6}{\put(0,9.2){\circle*{3}}}}%
\red{\advirecord{a7}{\put(0,18.2){\circle*{3}}}}%
\red{\advirecord{a8}{\put(0,27.2){\circle*{3}}}}%
\red{\advirecord{a9}{\put(0,36.2){\circle*{3}}}}%
\red{\advirecord{a10}{\put(0,45.2){\circle*{3}}}}%
\red{\advirecord{a11}{\put(0,54.2){\circle*{3}}}}%
\red{\advirecord{a12}{\put(0,63.2){\circle*{3}}}}%
\red{\advirecord{a13}{\put(6.3,56.9){\circle*{3}}}}%
\red{\advirecord{a14}{\put(12.6,50.6){\circle*{3}}}}%
\red{\advirecord{a15}{\put(18.9,44.3){\circle*{3}}}}%
\red{\advirecord{a16}{\put(25.2,38){\circle*{3}}}}%
\red{\advirecord{a17}{\put(31.5,31.7){\circle*{3}}}}%
\red{\advirecord{a18}{\put(37.8,25.4){\circle*{3}}}}%
\red{\advirecord{a19}{\put(44.1,19.1){\circle*{3}}}}%
\red{\advirecord{a20}{\put(50.4,12.8){\circle*{3}}}}%
\red{\advirecord{a21}{\put(56.7,6.5){\circle*{3}}}}%
\red{\advirecord{a22}{\put(63,0.2){\circle*{3}}}}%
\end{picture}
\bigskip
\end{center}
\adviplay{a23}
\adviplay{a24}
\adviplay{a25}
\adviplay{a1}
\adviplay{a2}
\adviwait
\adviplay[white]{a1}
\adviplay[white]{a2}
\adviplay[slidegreen]{a3}
\adviplay[slidegreen]{a4}

\begin{itemize}
\item[$\bullet$]
\textbf{berekenen:} wat is de verhouding tussen de zijde en de diagonaal?
$$\adviwait\mbox{\blue{Pythagoras:} }\mbox{ $\green{1 : \sqrt{2} = 1 : 1,\!4142135623\dots}$}\adviwait\smallskip$$

\item[$\bullet$]
\textbf{bewijzen:} is dit als een verhouding van gehele getallen te schrijven?
$$
\adviplay[slidered]{a5}
\adviplay[slidered]{a6}
\adviplay[slidered]{a7}
\adviplay[slidered]{a8}
\adviplay[slidered]{a9}
\adviplay[slidered]{a10}
\adviplay[slidered]{a11}
\adviplay[slidered]{a12}
\adviplay[slidered]{a13}
\adviplay[slidered]{a14}
\adviplay[slidered]{a15}
\adviplay[slidered]{a16}
\adviplay[slidered]{a17}
\adviplay[slidered]{a18}
\adviplay[slidered]{a19}
\adviplay[slidered]{a20}
\adviplay[slidered]{a21}
\adviplay[slidered]{a22}
\adviwait
%\adviplay[white]{a5}
%\adviplay[white]{a6}
%\adviplay[white]{a7}
%\adviplay[white]{a8}
%\adviplay[white]{a9}
%\adviplay[white]{a10}
%\adviplay[white]{a11}
%\adviplay[white]{a12}
%\adviplay[white]{a13}
%\adviplay[white]{a14}
%\adviplay[white]{a15}
%\adviplay[white]{a16}
%\adviplay[white]{a17}
%\adviplay[white]{a18}
%\adviplay[white]{a19}
%\adviplay[white]{a20}
%\adviplay[white]{a21}
%\adviplay[white]{a22}
%\adviplay{a23}
%\adviplay{a24}
%\adviplay[slidegreen]{a3}
%\adviplay[slidegreen]{a4}
\mbox{\blue{Pythagoras:} }\rlap{\red{\mbox{ niet mogelijk, \textsl{want}$\,$\dots}}}\phantom{\mbox{ ${1 : \sqrt{2} = 1 : 1,\!4142135623\dots}$}}$$

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{computerwiskunde}
\slidetitle{vier soorten}

\begin{itemize}
\item[$\bullet$]
\textbf{berekenen}\advirecord{b1}{\textbf{:} \textsl{getallen}}

\green{\advirecord{b2}{numerieke wiskunde}}\advirecord{b3}{, \blue{visualisatie, experimentatie}}

\medskip
\item[\advirecord{b4}{$\bullet$}]
\advirecord{b5}{\textbf{berekenen}\textbf{:} \textsl{formules}}

\green{\advirecord{b6}{computer algebra}}

\medskip
\item[$\bullet$]
\textbf{bewijzen}\advirecord{b7}{\textbf{:} \textsl{door de computer}}

\green{\advirecord{b8}{automatische stellingenbewijzers}}

\adviwait
\adviplay{b1}
\adviplay{b4}
\adviplay{b5}
\adviwait
\adviplay[slidegreen]{b2}
\adviplay[slidegreen]{b6}
\adviplay[slidegreen]{b8}
\adviwait
\adviplay{b7}

\medskip
\item[$\bullet$]
\textbf{bewijzen}\textbf{:} \textsl{door de mens}, met behulp van de computer
%\adviwait

\red{\advirecord{b9}{bewijsassistenten}}

\end{itemize}
\adviplay[slidegreen]{b9}
\adviwait
\adviplay[slidered]{b9}
\adviwait
\adviplay{b3}

\vfill
\end{slide}

\begin{slide}
\slidetitle{numerieke wiskunde: de Mandelbrot-verzameling}
\begin{center}
\includegraphics[height=10em]{\pics/mandelbrot.eps}
\end{center}
$$\green{z_0} = 0,\; \green{z_1} = z_0^2 + \red{c},\; \green{z_2} = z_1^2 + \red{c},\; \dots$$
$$\{\red{c}\in{\mathbb C} \;\;|\; \mbox{de rij $\green{z_i}$ gaat niet naar $\infty$}\}\bigskip\adviwait$$

\blue{hoe belangrijk is het dat iedere pixel in dit plaatje correct is?}

\vfill
\end{slide}

\begin{slide}
\slidetitle{numerieke wiskunde: het Mertens-vermoeden}
M{\"o}bius functie:
$$
\mu(n) =
\left\{
\begin{array}{rl}
0 & \mbox{als $n$ dubbele priemfactoren heeft} \\
1 & \mbox{als $n$ een even aantal verschillende priemfactoren heeft} \\
-1 & \mbox{als $n$ een oneven aantal verschillende priemfactoren heeft}
\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]{\pics/mimg2409.eps}
\qquad
\includegraphics[height=8em]{\pics/mimg1757.eps}
$\hspace{-1em}$
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{numerieke wiskunde: het Mertens-vermoeden (vervolg)}
Odlyzko \& te Riele, 1985: vermoeden van Mertens is \red{niet waar$\,$!} \\
\green{50 uur computertijd}
\smallskip

eerste $n$ waar het mis gaat heeft tientallen cijfers \\
indirect bewijs$\,$!
\smallskip
\adviwait

\green{2000 nulpunten van Riemann zeta functie op 100 decimalen nauwkeurig}

\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{computer algebra: een integraal uitrekenen}

\vspace{-.6em}
\vbox to 0pt{%
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\advirecord{c2}{\includegraphics[width=7em]{\pics/graph.eps}}
\vss}
\vspace{-1.3em}
Matlab, Mathematica, \green{\advirecord{c1}{Maple}}\adviplay{c1}, Magma
\adviwait
\adviplay[slidegreen]{c1}
\adviplay{c2}

\begin{quote}
\medskip
\texttt{> \blue{Int(ln(x)/(1 - x), x = 0..1);}}
$$\green{\int_0^1 {\ln x\over 1 - x} \,dx}\adviwait$$
\texttt{> \blue{value(\char`\%);}}
$$\green{-{\pi^2\over 6}}\adviwait$$
\texttt{> \blue{evalf(\char`\%);}}
$$\green{-1.64493406\red{\advirecord{c2}{8}}\adviplay[slidegreen]{c2}}\adviwait\adviplay[slidered]{c2}\medskip$$
\end{quote}
$$\blue{-1.64493406\red{6\mbox{\rlap{\textrm{8482264\dots}}}}}\leqno{\mbox{{c\rlap{orrecte uitkomst:}}}}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{automatische stellingenbewijzers: de systemen}
\textbf{TPTP} \\
\blue{Thousands of Problems for Theorem Provers} \\
\green{7068 problemen}
\medskip
\adviwait

\textbf{CASC} \\
\blue{C{ADE} ATP System Competition} \\
{Conference on Automated Deduction}, {Automated Theorem Prover}
\bigskip
\adviwait

winnaar 2008: \red{Vampire} \\
\green{169 van de 200 problemen opgelost}

tweede 2008: \red{E} \\
\green{164 van de 200 problemen opgelost}
\medskip
\adviwait

\red{Otter} $\,\approx\,$ \red{Prover9}

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

\begin{slide}
\slidetitle{automatische stellingenbewijzers: het Robbins-vermoeden}
is iedere \textbf{Robbins algebra} een Boolse algebra?
$$
\blue{
\begin{array}{c}
a \lor b = b \lor a \\
a \lor (b \lor c) = (a \lor b) \lor c \\
\neg(\neg(a \lor b) \lor \neg (a \lor \neg b)) = a
\end{array}
}
\medskip
\smallskip
\adviwait
$$
Bill McCune $+$ \red{EQP}, 1996: \red{inderdaad!} \\
\green{8 dagen computertijd} \\
{bewijs van 34 regels}
\adviwait
\medskip
\smallskip

\blue{automatische stellingenbewijzers kunnen tot nog toe:}
\begin{itemize}
\item[$\bullet$]
{`puzzels' waarin heel veel gevallen moeten worden onderzocht}

\item[$\bullet$]
{elementaire stapjes in een bewijs}

\end{itemize}

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

\begin{slide}
\slidetitle{bewijsassistenten}
\begin{itemize}
\item[$\bullet$]
\textbf{numerieke wiskunde} en \textbf{computer algebra:} \green{geen bewijzen}

\medskip
\item[$\bullet$]
\textbf{\blue{\advirecord{d}{automatische}}\adviplay{d} stellingenbewijzers:} \green{geen interessante wiskunde}
%\adviwait

\medskip
\item[$\bullet$]
\textbf{bewijsassistenten:} \green{w\'el bewijzen \& w\'el interessante wiskunde}
\adviwait
\medskip

\textsl{de prijs die moet worden betaald:} \\
\red{gebruiker moet veel zelf doen}
\bigskip
\smallskip
\adviwait
\adviplay[slideblue]{d}

bewijsassistenten $=$ \textbf{\blue{interactieve} stellingenbewijzers} \\
\green{\red{samenspel} van mens en computer}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{vier bewijsassistenten}
\slidetitle{100 leuke stellingen, 80 geformaliseerd}
\vbox to 0pt{\small
\vspace{-1.65em}
\begin{tabular}{lr}
\enskip 1. The Irrationality of the Square Root of 2 & \llap{$\ge \blue{\sf 17}$} \\
\noalign{\vspace{-\smallskipamount}}
\enskip 2. {Fundamental Theorem of Algebra} & 4 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 3. The Denumerability of the Rational Numbers & 6 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 4. Pythagorean Theorem & 6 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 5. {Prime Number Theorem} & 2 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 6. {G\"odel's Incompleteness Theorem} & 3 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 7. Law of Quadratic Reciprocity & 4 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 8. The Impossibility of Trisecting the Angle and Doubling the Cube$\quad$ & 1 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 9. The Area of a Circle & 1 \\
\noalign{\vspace{-\smallskipamount}}
10. Euler's Generalization of Fermat's Little Theorem & 4 \\
\noalign{\vspace{-\smallskipamount}}
11. The Infinitude of Primes & 6 \\
\noalign{\vspace{-\smallskipamount}}
\green{12. The Independence of the Parallel Postulate} & \green{0} \\
\noalign{\vspace{-\smallskipamount}}
13. {Polyhedron Formula} & 1 \\
\noalign{\vspace{-\smallskipamount}}
\phantom{00. }\dots
\end{tabular}
\vss}
\vbox to 0pt{
\vspace{14.5em}
\small
\adviwait
\hfill {google:} \fbox{\strut \enskip$\!$\red{100 theorems}\enskip}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{de beste bewijsassistenten}
\red{vijf systemen} serieus gebruikt voor {wiskunde}:
\bigskip
\medskip

\begin{center}
\quad
\begin{tabular}{lcr}
\llap{\setbox0=\hbox{{\advirecord{e1}{$\mbox{{HOL}}\;\Bigg\{\quad\quad$}}}\ht0=-1em\dp0=-1em\raise -.92em\box0}%
\green{HOL Light} &$\hspace{5em}$& \green{69} \\
\noalign{\smallskip}
\gray{\advirecord{e4}{ProofPower}}\adviplay{e4} && \gray{\advirecord{e5}{42}}\adviplay{e5} \\
\noalign{\smallskip}
{Isabelle} && 40 \\
\noalign{\smallskip}
{Coq} && 39 \\
\noalign{\smallskip}
\blue{\advirecord{e2}{Mizar}}\adviplay{e2} && \blue{\advirecord{e3}{45}}\adviplay{e3} \\
\end{tabular}
\end{center}
\adviwait
\adviplay{e1}
\adviwait
\adviplay[slidegray]{e4}
\adviplay[slidegray]{e5}
\adviwait
\adviplay[slideblue]{e2}
\adviplay[slideblue]{e3}

\vfill
\end{slide}

\begin{slide}
\slidetitle{HOL Light}

\vspace{-.6em}
\vbox to 0pt{%
\includegraphics[height=1em]{\pics/uk.eps}
\includegraphics[height=1em]{\pics/usa.eps}
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=7em]{\pics/johnh.eps}
\vss}

\vspace{2em}
in lange traditie: \\
\blue{LCF} $\to$ HOL $\to$ HOL Light \\
Stanford, US $\to$ Cambridge, UK $\to$ Portland, US
\bigskip

\red{John Harrison}

\adviwait
\vbox to 0pt{%
\hfill
\includegraphics[width=7em]{\pics/pentium.eps}
\vss}
\vspace{-1.385em}
bewijst floating point hardware correct bij \blue{Intel} \\
\adviwait
formaliseert wiskunde in zijn vrije tijd
\bigskip
\adviwait

\green{bijzonder elegant systeem} \\
\green{makkelijk uit te breiden}

\textsl{niet gebruikersvriendelijk}

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

\begin{slide}
\slidetitle{Isabelle}

\vspace{-.6em}
\vbox to 0pt{%
\includegraphics[height=1em]{\pics/uk.eps}
\includegraphics[height=1em]{\pics/germany.eps}
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\vss}

\vspace{2em}
soort `opvolger' van HOL
\medskip
\smallskip

\textsl{samenwerking tussen twee universiteiten:}

\blue{Cambridge, UK} \\
vooral: computerveiligheid

\blue{M\"unchen, Duitsland} \\
vooral: wiskunde
\bigskip
\adviwait

\red{gebalanceerd systeem}

\green{mooie bewijstaal} \\
\green{krachtige automatisering}

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

\begin{slide}
\slidetitle{Coq}

\vspace{-.6em}
\vbox to 0pt{%
\includegraphics[height=1em]{\pics/france.eps}
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\vss}

\vspace{2em}
{INRIA} en \blue{Microsoft} \\
\blue{Institut National de Recherche en Informatique et en Automatique}
\bigskip
\adviwait

{systeem met de \red{indrukwekkendste formalisatie} tot nu toe} \\
{systeem dat {wij in Nijmegen} gebruiken}
\bigskip
\adviwait

\green{ge\"\i ntegreerde programmeertaal} \\
$\approx$ {Haskell}
\smallskip
\adviwait

\green{wiskundige expressief}

\green{\textbf{intu\"\i tionistisch}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{intu\"\i tionistische wiskunde}

\vspace{-.6em}
\vbox to 0pt{%
\includegraphics[height=1em]{\pics/netherlands.eps}
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=6em]{\pics/brouwer.eps}
\vss}

\vspace{2em}
\red{Luitzen Egbertus Jan Brouwer} \\
{pionier van de \blue{topologie}}
\bigskip

proefschrift, 1907 \\
\textbf{Over de grondslagen van de wiskunde}

\green{niet valide om over een re\"eel getal $x$ te redeneren \\
`\'of $x$ is nul, \'of $x$ is ongelijk aan nul}'

{`{uitgesloten derde}'}
\bigskip
\smallskip
\adviwait

\blue{tussenwaardestelling} intu\"\i tionistisch niet bewijsbaar

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

\begin{slide}
\slidetitle{Mizar}

\vspace{-.6em}
\vbox to 0pt{%
\includegraphics[height=1em]{\pics/poland.eps}
\includegraphics[height=1em]{\pics/japan.eps}
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=6em]{\pics/andrzej.eps}
\vss}

\vspace{2em}
\red{Andrzej Trybulec} \\
Bia\l ystok, \blue{Polen}
\smallskip

ook: Nagano, \blue{Japan}
\bigskip
\medskip
\adviwait

\green{wiskundigste van de bewijsassistenten}
\medskip

\green{grootste bibliotheek met geformaliseerde wiskunde} \\
2,1 miljoen regels code
\medskip

{gebruikersvriendelijk} \\
\adviwait
\textsl{soms moeilijk te begrijpen}

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

\begin{slide}
\sectiontitle{geformaliseerde stellingen}
\slidetitle{de hoofdstelling van de algebra}

\vspace{-.6em}
\vbox to 0pt{%
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=6em]{\pics/gauss.eps}
\vss}
\vspace{-1.3em}
\red{Carl Friedrich Gauss, 1799} \\
\green{Mizar: Robert Milewski, 2000 \\
HOL Light: John Harrison, 2000} \\
\red{Hellmut Kneser, 1940} \\
\green{Coq: Herman Geuvers e.a., 2000}
\adviwait

%complexe getallen:
$${x^2 = {-1}\rlap{$\;$\white{\advirecord{f1}{?}}\adviplay{f1}}}\adviwait\adviplay[white]{f1}$$
$$x = \red{i = \sqrt{-1}}\adviwait\smallskip$$

\blue{welke polynomiale vergelijkingen kunnen we nu oplossen?}
$$x^2 = \red{i}\rlap{$\;${?}}$$

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

\begin{slide}
\slidetitle{de priemgetalstelling}
\red{Paul Erd\"os en Atle Selberg, 1949} \\
\green{Isabelle: Jeremy Avigad, 2004} \\
\red{Jacques Hadamard, Charles Jean de la Vall\'ee-Poussin, 1896} \\
\green{HOL Light: John Harrison, 2008}
\medskip
\adviwait

aantal priemgetallen $\le$ gegeven getal:
\begin{eqnarray*}
\pi(1000000000000) &=& 37607912018 \\
\noalign{\smallskip}
\adviwait
{1000000000000\over\ln(1000000000000)} &=& 36191206825,\!27\!\dots \\
\noalign{\smallskip}
\adviwait
\int_2^{1000000000000} {dx\over\ln(x)} &=& 37607950279,\!75\!\dots \\
\noalign{\vspace{-.8\bigskipamount}}
\adviwait
\end{eqnarray*}

\blue{wat is de verhouding in de limiet van het aantal getallen naar $\infty$?}

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

\begin{slide}
\slidetitle{de stelling over Jordan-krommen}
\red{Oswald Veblen, 1905} \\
\green{HOL Light: Tom Hales, 2005 \\
Mizar: Artur Korni\l owicz e.a., 2005}
\bigskip
\adviwait

\begin{center}
\includegraphics[width=20em]{\pics/jordan.eps}

\strut\hspace{1em}Jordan-krommen\hspace{3em}geen Jordan-krommen
\end{center}
\bigskip
\adviwait

\blue{in hoeveel stukken verdeelt een Jordan-kromme het platte vlak?}

\vfill
\end{slide}

\begin{slide}
\slidetitle{de eerste onvolledigheidsstelling}

\vspace{-.6em}
\vbox to 0pt{%
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=6em]{\pics/goedel.eps}
\vss}
\vspace{-1.3em}
\red{Kurt G\"odel, 1931} \\
\green{Boyer-Moore prover: Natarajan Shankar, 1986 \\
Coq: Russell O'Connor, 2003 \\
HOL Light: John Harrison, 2005}
\bigskip
\adviwait

de G\"odel-zin:
\begin{center}
`\red{deze zin is niet bewijsbaar}'
\end{center}
\medskip
\adviwait

als deze zin waar is, zijn er onbewijsbare ware zinnen \gray{(onvolledigheid)} \\
als deze zin onwaar is, zijn er bewijsbare onware zinnen \gray{(inconsistentie)}
\adviwait
\bigskip

\blue{is er een bewijssysteem waarin waarheid en bewijsbaarheid samenvalt?}

\vfill
\end{slide}

\begin{slide}
\slidetitle{de vierkleurenstelling}

\vspace{-.6em}
\vbox to 0pt{%
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\includegraphics[width=6em]{\pics/gonthier.eps}
\vss}
\vspace{-1.3em}
\red{Kenneth Appel en Wolfgang Haken, 1976 \\
Neil Robertson e.a., 1996} \\
\green{Coq: Georges Gonthier, 2004}
\bigskip
\adviwait

\begin{center}
\includegraphics[width=18em]{\pics/fourcolor.eps}\hspace{5em}\strut
\end{center}
\medskip
\adviwait

\blue{kan \textsl{iedere} kaart met maar vier verschillende kleuren worden gekleurd?}

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

\begin{slide}
\sectiontitle{zelf formaliseren?}
\slidetitle{wetenschappelijk onderzoek}
tijd voor het formaliseren van om \'e\'en bladzijde uit een leerboek: \\
\green{\'e\'en volle werkweek $\approx$ 40 uur}
\smallskip
\adviwait

lengte van een formalisatie van \'e\'en bladzijde uit een leerboek: \\
\green{een aantal computerschermen vol $\approx$ 200 regels}
\smallskip

\green{$\approx$ een kwartier per regel} \\
\red{moeilijk\exclspace!}
\bigskip
\adviwait

\red{toch proberen Mizar te leren?}
\smallskip

\blue{\textbf{writing a Mizar article in nine easy steps}}
\blue{\small\texttt{http://www.cs.ru.nl/\char`\~freek/mizar/mizman.pdf}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{bewijzen \hfill \black{\small Marjolein Kool}}
\vbox to 0pt{
\vspace{-1.4em}
\def\mizar#1{\strut\rlap{\hspace{160pt}\texttt{\strut #1}}}
\begin{flushleft}\footnotesize
\offinterlineskip
\mizar{}%
\advirecord{c1}{Een bolleboos riep laatst met zwier} \\
\advirecord{c2}{\mizar{theorem}}%
\advirecord{c3}{gewapend met een vel A-vijf:} \\
\red{\advirecord{c4}{\mizar{\ \ not ex n st for m holds n >= m}}}%
\advirecord{c5}{Er is geen allergrootst getal,} \\
\advirecord{c6}{\mizar{proof}}%
\advirecord{c7}{dat is wat ik bewijzen ga.} \\
\mizar{}%
\advirecord{c8}{Stel, dat ik u nu zou bedriegen} \\
\green{\advirecord{c9}{\mizar{\ \ assume not thesis;}}}%
\advirecord{c10}{en hier een potje stond te jokken,} \\
\green{\advirecord{c11}{\mizar{\ \ then consider n such that}}}%
\advirecord{c12}{dan ik zou zonder overdrijven} \\
\white{\advirecord{cx1}{\mizar{\ \ let n;}}}%
\green{\advirecord{c13}{\mizar{\rlap{\advirecord{c37}{A1:}}\ \ \ \ for m holds n \char`\>= m;}}}%
\advirecord{c14}{het grootste kunnen op gaan noemen.} \\
\mizar{}%
\advirecord{c15}{Maar ben ik klaar, roept u gemeen:} \\
\green{\advirecord{c16}{\mizar{\ \ set n' = n + 2;}}}%
\advirecord{c17}{`Vermeerder dat getal met twee!'} \\
\mizar{}%
\advirecord{c18}{En zien we zeker en gewis} \\
\white{\advirecord{cx2}{\mizar{\ \ n + 2 > n by XREAL\char`\_1:31;}}}%
\green{\advirecord{c19}{\mizar{\ \ n' > n\rlap{\white{\advirecord{c35}{;}}}\ \advirecord{c38}{by XREAL\char`\_1:31;}}}}%
\advirecord{c20}{dat dit toch niet het grootste was.} \\
{\mizar{\ \ \ \ \ \ \ \white{\advirecord{c33}{*4}}}}%
\advirecord{c22}{En gaan we zo nog door een poos,} \\
\green{\advirecord{c23}{\mizar{\ \ then not for m holds n >= m;}}}%
\advirecord{c24}{dan merkt u: dit is onbegrensd.} \\
\mizar{}%
\advirecord{c25}{En daarmee heb ik q.e.d.} \\
\white{\advirecord{cx3}{\mizar{\ \ hence thesis;}}}%
\green{\advirecord{c26}{\mizar{\ \ hence contradiction\rlap{\white{\advirecord{c36}{;}}}\ \advirecord{c39}{by A1;}}}}%
\advirecord{c27}{Ik ben hier diep gelukkig door.} \\
{\mizar{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \white{\advirecord{c34}{*1}}}}%
\advirecord{c29}{`Zo gaan', zei hij voor hij bezwijmde,} \\
\advirecord{c30}{\mizar{end;}}%
\advirecord{c31}{`bewijzen uit het ongedichte'.}
\end{flushleft}
\vss
\adviplay{c1}
\adviplay{c3}
\adviplay{c5}
\adviplay{c7}
\adviplay{c8}
\adviplay{c10}
\adviplay{c12}
\adviplay{c14}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c22}
\adviplay{c24}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviwait
\adviplay[slideblue]{x1}
\adviplay[slideblue]{x2}
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay[slidegreen]{c1}
\adviplay[slidegreen]{c2}
\adviplay[slidegreen]{c3}
\adviwait
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay[slidegreen]{c4}
\adviplay[slidegreen]{c5}
\adviwait
\adviplay{c4}
\adviplay{c5}
\adviplay[slidegreen]{c6}
\adviplay[slidegreen]{c7}
\adviwait
\adviplay{c6}
\adviplay{c7}
\adviplay[slidegreen]{c8}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c10}
\adviwait
\adviplay{c8}
\adviplay{c9}
\adviplay{c10}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c12}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c14}
\adviwait
\adviplay{c11}
\adviplay{c12}
\adviplay{c13}
\adviplay{c14}
\adviplay[slidegreen]{c15}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c17}
\adviwait
\adviplay{c15}
\adviplay{c16}
\adviplay{c17}
\adviplay[slidegreen]{c18}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c20}
\adviplay[slidegreen]{c35}
\adviwait
\adviplay{c18}
\adviplay{c19}
\adviplay{c20}
\adviplay{c35}
\adviplay[slidegreen]{c22}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c24}
\adviwait
\adviplay{c22}
\adviplay{c23}
\adviplay{c24}
\adviplay[slidegreen]{c25}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c27}
\adviplay[slidegreen]{c36}
\adviwait
\adviplay{c25}
\adviplay{c26}
\adviplay{c27}
\adviplay{c36}
\adviplay[slidegreen]{c29}
\adviplay[slidegreen]{c30}
\adviplay[slidegreen]{c31}
\adviwait
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay{c30}
\adviplay[slidered]{c33}
\adviplay[slidered]{c34}
\adviwait
\adviplay[white]{c34}
\adviplay[white]{c36}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c33}
\adviplay[white]{c35}
\adviplay[slidegreen]{c38}
\adviwait
\adviplay{c37}
\adviplay{c38}
\adviplay{c39}
\adviplay[slidered]{c4}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c38}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c9}
\adviplay[white]{c11}
\adviplay[white]{c13}
\adviplay[white]{c37}
\adviplay[white]{c16}
\adviplay[white]{c19}
\adviplay[white]{c38}
\adviplay[white]{c23}
\adviplay[white]{c26}
\adviplay[white]{c39}
\adviplay[slidegreen]{cx1}
\adviplay[slidegreen]{cx2}
\adviplay[slidegreen]{cx3}
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Pythagore\"\i sche drietallen: een formule}

\vspace{-.6em}
\vbox to 0pt{%
\vss}
\vspace{-1.385em}
\vbox to 0pt{%
\hfill
\begingroup
\setlength{\unitlength}{.5pt}
\blue{
\begin{picture}(80,60)(0,0)
\put(0,0){\line(1,0){80}}
\put(0,0){\line(0,1){60}}
\put(80,0){\line(-4,3){80}}
\put(39,-11){\makebox(0,0){\small $b$}}
\put(-10,28.5){\makebox(0,0){\small $a$}}
\put(49,37){\makebox(0,0){\small $c$}}
\put(0,6){\line(1,0){6}}
\put(6,0){\line(0,1){6}}
\end{picture}}
\endgroup
\vss}
\vspace{-1.3em}
een oplossing van
$$\blue{a^2 + b^2 = c^2}\medskip$$
\green{\advirecord{g1}{zonder gemeenschappelijke delers}}\adviplay{g1} is altijd van de vorm:
$$\red{a = m^2 - n^2 \qquad b = 2mn \qquad c = m^2 + n^2}\medskip$$
\adviwait
\textbf{voorbeelden}
$$\begin{array}{ccrcrcr}
m = 2 \qquad n = 1 & \quad\to\quad & 3^2 & + & 4^2 & = & 5^2 \\
\noalign{\vspace{-\smallskipamount}}
m = 3 \qquad n = 2 & \to & 5^2 & + & 12^2 & = & 13^2 \\
\noalign{\vspace{-\smallskipamount}}
m = 4 \qquad n = 1 & \to & 15^2 & + & 8^2 & = & 17^2 \\
\noalign{\vspace{-\smallskipamount}}
m = 4 \qquad n = 3 & \to & 7^2 & + & 24^2 & = & 25^2 \adviwait\\
\noalign{\vspace{-\smallskipamount}}
& \green{\not\to} & \green{9^2} & \green{+} & \green{12^2} & \green{=} & \green{15^2}
\adviplay[slidegreen]{g1}
\end{array}$$

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

\begin{slide}
\slidetitle{Pythagore\"\i sche drietallen: `formal proof sketch'}
\vspace{-1.9em}
\begin{alltt}
reserve a,b,c,m,n for Nat;\medskip
let a,b,c; assume \advirecord{z1}{a^2 + b^2 = c^2}\adviplay[slidegreen]{z1};
assume \advirecord{z2}{a,b are_relative_prime}\adviplay[slidegreen]{z2};\adviwait\adviplay[black]{z1}\adviplay[slidered]{z2}
then \advirecord{z3}{a is odd or b is odd}\adviplay[slidegreen]{z3};{\adviwait\adviplay[black]{z2}\adviplay[slidered]{z3}} assume \advirecord{z4}{a is odd}\adviplay[slidegreen]{z4};\adviwait\adviplay[black]{z3}\adviplay[black]{z4}\medskip
\advirecord{z5}{ex m,n st \advirecord{z5a}{a = m^2 - n^2} & \advirecord{z5b}{b = 2*m*n} & \advirecord{z5c}{c = m^2 + n^2}
proof}\adviplay[slidegreen]{z5}\adviplay[slidegreen]{z5a}\adviplay[slidegreen]{z5b}\adviplay[slidegreen]{z5c}\adviwait\adviplay[black]{z5}\adviplay[black]{z5a}\adviplay[black]{z5b}\adviplay[black]{z5c}
  \advirecord{z6}{b is even}\adviplay[slidegreen]{z6};{\adviplay[slidered]{z1}\adviplay[slidered]{z4}\adviwait\adviplay[slidered]{z6}} \advirecord{z7}{c is odd}\adviplay[slidegreen]{z7};\adviwait\adviplay[black]{z4}\adviplay[black]{z6}\adviplay[black]{z7}\adviplay[slidered]{z2}
X: \red{\advirecord{z8}{(c + a)/2,(c - a)/2 are_relative_prime}}\adviplay[slidegreen]{z8};\adviwait\adviplay[black]{z2}\adviplay[black]{z8}
  \advirecord{z9}{((c + a)/2)*((c - a)/2) = (c^2 - a^2)/4 .= (b/2)^2}\adviplay[slidegreen]{z9};\adviwait\adviplay[black]{z1}\adviplay[slidered]{z9}
  then \red{\advirecord{z10}{((c + a)/2)*((c - a)/2) is square}}\adviplay[slidegreen]{z10};\adviwait\adviplay[black]{z9}\adviplay[slidered]{z8}\adviplay[slidered]{z10}
  then \green{\advirecord{z11}{(c + a)/2 is square & (c - a)/2 is square}}\adviplay[slidegreen]{z11} by X;\adviwait\adviplay[black]{z8}\adviplay[black]{z10}\adviplay[slidered]{z11}
  consider m,n such that \advirecord{z11a}{(c + a)/2 = m^2}\adviplay[slidegreen]{z11a} & \advirecord{z11b}{(c - a)/2 = n^2}\adviplay[slidegreen]{z11b};\toolong\adviwait
  take m,n;\adviplay[black]{z11}\adviplay[slideblue]{z5a}\adviplay[slideblue]{z5b}\adviplay[slideblue]{z5c}
\end{alltt}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Pythagore\"\i sche drietallen: `formal proof sketch' (vervolg)}
\begin{flushleft}
\vspace{-.5em}
\begin{color}{slidegray}
\verb|  consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;|\toolong\\
\verb|  take m,n;|\\
\end{color}
\verb|  thus a = (c + a)/2 - (c - a)/2 .= m^2 - n^2;|\\
\verb|  b^2 = (c + a)*(c - a) .= 4*m^2*n^2 .= (2*m*n)^2;|\\
\verb|  hence b = 2*m*n;|\\
\verb|  thus c = (c + a)/2 + (c - a)/2 .= m^2 + n^2;|\\
\verb|end;|
\end{flushleft}
\adviwait
\medskip
\smallskip

syntactisch correct \\
\adviwait
semantisch correct \\
\adviwait
\red{te kort door de bocht}

\green{stappen te groot \\
relaties tussen de stappen niet expliciet}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Pythagore\"\i sche drietallen: fragment van de uitgewerkte formalisatie}
\begin{flushleft}
\vspace{-.5em}
\advirecord{x1}{\tt\ then}\\
\advirecord{x2}{\tt X: (c + a)/2,(c - a)/2 are\char`_relative\char`_prime}\advirecord{x3}{\tt\ by Lm3}\advirecord{x4}{;}\\
\advirecord{x5}{\tt\ ((c + a)/2)*((c - a)/2) =}\advirecord{x6}{\tt\ ((c + a)*(c
- a))/(2*2)}\\
\advirecord{x7}{\ \ \ by }\advirecord{x7a}{REAL\char`_1:35}\\
\advirecord{x8}{\ \ .= }\advirecord{x9}{\tt (c\^{}2 - a\^{}2)/4}\advirecord{x10}{\tt\ by }\advirecord{x10a}{SQUARE\char`_1:67}\\
\advirecord{x11}{\tt\ \ .= (b\^{}2)/(2*2)}\advirecord{x12}{\tt\ by H1,}\advirecord{x12a}{INT\char`_1:3}\\
\advirecord{x13}{\tt\ \ .= (b\^{}2)/(2\^{}2)}\advirecord{x14}{\tt\ by }\advirecord{x14a}{SQUARE\char`_1:def 3}\\
\advirecord{x15}{\tt\ \ .= (b/2)\^{}2}\advirecord{x16}{\tt\ by }\advirecord{x16a}{SQUARE\char`_1:69}\advirecord{x17}{\tt;}\\
\advirecord{x18}{\tt\ then ((c + a)/2)*((c - a)/2) is square}\advirecord{x19}{\tt\ by A1,Def1}\advirecord{x20}{\tt ;}\\
\advirecord{x21}{\tt\ then (c + a)/2 is square \& (c - a)/2 is square by X}\advirecord{x22}{\tt ,Lm4}\advirecord{x23}{\tt ;}\\
\advirecord{x24}{\tt\ then (ex m st m\^{}2 = (c + a)/2) \&}\\
\advirecord{x25}{\tt\ \ (ex n st n\^{}2 = (c - a)/2)}\advirecord{x26}{\tt\ by Def1}\advirecord{x27}{\tt ;}\\
\advirecord{x28}{\tt\ then }\advirecord{x29}{\tt consider m,n such that}\\
\advirecord{x30}{\tt A9:}\advirecord{x31}{\tt\ m\^{}2 = (c + a)/2 \& n\^{}2 = (c - a)/2;}
\end{flushleft}
\adviplay{x2}
\adviplay{x4}
\adviplay{x5}
\adviplay{x9}
\adviplay{x15}
\adviplay{x17}
\adviplay{x18}
\adviplay{x20}
\adviplay{x21}
\adviplay{x23}
\adviplay{x29}
\adviplay{x31}
\adviwait
\adviplay[slidegreen]{x6}
\adviplay[slidegreen]{x8}
\adviplay[slidegreen]{x11}
\adviplay[slidegreen]{x13}
\adviplay[slidegreen]{x24}
\adviplay[slidegreen]{x25}
\adviplay[slidegreen]{x27}
\adviwait
\adviplay[slidered]{x1}
\adviplay[slidered]{x3}
\adviplay[slidered]{x7}
\adviplay[slidered]{x7a}
\adviplay[slidered]{x10}
\adviplay[slidered]{x10a}
\adviplay[slidered]{x12}
\adviplay[slidered]{x12a}
\adviplay[slidered]{x14}
\adviplay[slidered]{x14a}
\adviplay[slidered]{x16}
\adviplay[slidered]{x16a}
\adviplay[slidered]{x19}
\adviplay[slidered]{x22}
\adviplay[slidered]{x26}
\adviplay[slidered]{x28}
\adviplay[slidered]{x30}
\adviwait
\adviplay{x6}
\adviplay{x8}
\adviplay{x11}
\adviplay{x13}
\adviplay{x24}
\adviplay{x25}
\adviplay{x27}
\adviplay{x1}
\adviplay{x3}
\adviplay{x7}
\adviplay{x7a}
\adviplay{x10}
\adviplay{x10a}
\adviplay{x12}
\adviplay{x12a}
\adviplay{x14}
\adviplay{x14a}
\adviplay{x16}
\adviplay{x16a}
\adviplay{x19}
\adviplay{x22}
\adviplay{x26}
\adviplay{x28}
\adviplay{x30}
\adviwait
\adviplay[slidered]{x7a}
\adviplay[slidered]{x10a}
\adviplay[slidered]{x12a}
\adviplay[slidered]{x14a}
\adviplay[slidered]{x16a}

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

\begin{slide}
\sectiontitle{een zeer korte geschiedenis van de wiskunde}
\slidetitle{de drie revoluties}

\begin{tabular}{c}
\adviwait
\includegraphics[height=8em]{\pics/euclid.eps} \\
Euclid \\
\textbf{bewijzen}
\end{tabular}\adviwait\hfill
\begin{tabular}{c}
\includegraphics[height=8em]{\pics/cauchy.eps} \\
Cauchy \\
\textbf{rigoreus}
\end{tabular}\adviwait\hfill
\begin{tabular}{c}
\includegraphics[height=8em]{\pics/debruijn.eps} \\
de Bruijn \\
\red{\textbf{formeel}}
\end{tabular}\hspace{0em}

\vfill
\end{slide}

\end{document}