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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large bewijzen in de computer}

Freek Wiedijk \\
\advirecord{a2}{\rlap{Radboud Universiteit Nijmegen}}\advirecord{a1}{Katholieke Universiteit Nijmegen}
\adviplay{a1}

Nationale Wiskunde Dagen \\
Noordwijkerhout \\
2004 02 06, 16:15
\adviwait
\adviplay[white]{a1}
\adviplay{a2}

\end{slide}

\begin{slide}
\slidetitle{principia mathematica}
\red{wiskunde in volledig detail in een formele taal}
%\adviwait

\begin{itemize}
\item[] \textbf{Leibniz,} eind 17de eeuw
\begin{itemize}
\begingroup
\small
\item[] uitvinder van differenti{\"e}ren en integreren
\vspace{-\smallskipamount}
\item[] bouwer van {\'e\'e}n van de eerste rekenmachines: $\times$, $\div$, $\surd$
\vspace{-\smallskipamount}
\endgroup
\smallskip
\item[] \green{lingua characteristica universalis} (universele taal)
\vspace{-\smallskipamount}
\item[] \green{calculus ratiocinator}
\end{itemize}
\adviwait
\item[] \textbf{Boole,} {The Calculus of Logic,} 1848
\vspace{-\smallskipamount}
\item[] \textbf{Frege,} {Begriffsschrift,} 1879
\adviwait
\item[] \textbf{Peano,} tijdschrift \red{Rivista di Matematica}, 1891-1906
\vspace{-\smallskipamount}
%\adviwait
\item[] \textbf{Russell \& Whitehead}, \red{Principia Mathematica}
\begin{itemize}
\item[] drie delen: 1910, 1912, 1913
\end{itemize}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\adviembed{xvieww /home/freek/talks/dagen/pics/principia.jpg}\adviwait[1]%
\slidetitle{automath}
computer $\;\to\;$ \red{bewijzen in volledig detail uitwerken wordt praktisch}
\adviwait
\smallskip

\green{eerste ter wereld:} \textbf{de Bruijn,} Eindhoven
\vspace{-\smallskipamount}
\begin{eqnarray*}
\mbox{`de automath'} &=& \mbox{computer om wiskunde mee te controleren} \\
\mbox{\red{automath}} &=& \mbox{\red{taal om  wiskunde in op te schrijven}}
\end{eqnarray*}
1968: eerste idee{\"e}n \\
jaren zeventig: groot onderzoeksproject
\medskip
\adviwait

\textbf{Jutting,} 1977: vertaling van een heel wiskundeboek

\dashskip dik pak computertekst \\
\dashskip controle op correctheid: paar uur computertijd \\
\adviwait
\dashskip \green{(tegenwoordig: een halve seconde)}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{wiskunde in de computer}
\slidetitle{berekenen en bewijzen}
\green{de twee activiteiten van de wiskundige}
\begin{itemize}
\item[$\bullet$] \textbf{berekenen}

het gaat om het antwoord:
\red{wat?}
\item[$\bullet$] \textbf{bewijzen}

het gaat om het begrip:
\red{waarom?}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{is bewijzen nog wel van deze tijd?}
\textbf{middelbaar onderwijs:} bewijzen wordt nauwelijks meer onderwezen
\green{
\begin{itemize}
\advirecord{b1}{\item[$\bullet$] er is geen grootste priemgetal}
\advirecord{b2}{\item[$\bullet$] decimalen van $\sqrt 2\,=${\footnotesize$\;$1.41421356237309504880168872420969807856967187537694807317\dots} herhalen niet}
\advirecord{b3}{\item[$\bullet$] er zijn meer re{\"e}le getallen dan natuurlijke getallen}
\advirecord{b4}{\item[$\bullet$] er zijn evenveel punten in een lijn als punten in het vlak}
\medskip
\end{itemize}
}
\adviwait

\textbf{universitair onderzoek:} computer-experimenten
steeds belangrijker \\
\dashskip {\dots} nemen de plaats van bewijzen over?
\medskip
\adviwait

\blue{bewijzen spelen tegenwoordig een rol in de \textbf{informatica}} \\
\red{kritische hardware/software mag geen `bugs' hebben}
\adviwait
\adviplay[slidegreen]{b1}
\adviwait
\adviembed{xvieww /home/freek/talks/dagen/pics/pandarve.jpg}
\adviwait
\adviplay[slidegreen]{b2}
\adviwait
\adviplay[slidegreen]{b3}
\adviwait
\adviplay[slidegreen]{b4}

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

\begin{slide}
\slidetitle{wiskunde in de computer}
\begin{itemize}
\item[$\bullet$] \textbf{numeriek}
\begin{center}
\advirecord{d1}{berekeningen}\advirecord{d2}{\llap{getallen}}\adviplay{d1}: computer $\to$ mens$\qquad$
\end{center}
\adviwait

\item[$\bullet$] \textbf{computer algebra}
\begin{center}
\advirecord{d3}{berekeningen}\advirecord{d4}{\llap{formules}}\adviplay{d3}: computer $\to$ mens$\qquad$
\end{center}
\adviwait
\adviplay[white]{d1}
\adviplay{d2}
\adviplay[white]{d3}
\adviplay{d4}
\adviwait

\item[$\bullet$] \textbf{stellingenbewijzers}
\begin{center}
bewijzen: computer $\to$ mens
\end{center}
\adviwait

\item[$\bullet$] \textbf{\advirecord{c}{bewijscheckers}\adviplay{c}}
\begin{center}
bewijzen: mens $\to$ computer
\smallskip
\adviwait
\adviplay[slidered]{c}
\end{center}
\begin{flushright}
\green{(computer kijkt alleen of het klopt)}
\end{flushright}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{numeriek}
\slidetitle{het vermoeden van Mertens}
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]{/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{het vermoeden van Mertens (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}
\sectiontitle{computer algebra}
\slidetitle{symbolische integratie}
\texttt{> \red{Int(ln(x)/(1 - x),x = 0..1);}}
$$\int_0^1 {\ln x\over 1 - x} \,dx$$
\adviwait
\texttt{> \red{value(\char`\%);}}
$$-{\pi^2\over 6}$$
\adviwait

\blue{het algoritme van Risch}

integraal uitdrukken in `elementaire functies' \green{$\surd$, $\ln$, $e^x$, $\sin$, $\arcsin$, \dots} \\
-- zegt of het kan \\
-- geeft het antwoord {als} het kan

\vfill
\end{slide}

\begin{slide}
\slidetitle{mathXpert}
populaire computer algebra systemen
\begin{itemize}
\item[$\bullet$] \red{maple}
\item[$\bullet$] \red{mathematica}
\smallskip
\end{itemize}
\adviwait

computer algebra voor het onderwijs
\begin{itemize}
\item[$\bullet$] \textbf{mathXpert} \\
Beeson, 1997
\smallskip
%\adviwait

\green{niet heel krachtig} \\
\green{wel heel duidelijk}

-- formules zien er uit als in de leerboekjes \\
-- niet alleen de antwoorden maar ook de berekeningen

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\adviembed{xvieww /home/freek/talks/dagen/pics/mathpert.gif}\adviwait[1]%
\sectiontitle{automatische stellingenbewijzers}
\slidetitle{het vermoeden van Robbins}
computers \\
\dashskip {\dots} kunnen binnenkort beter schaken dan mensen \\
\adviwait
\dashskip {\dots} kunnen binnenkort \red{beter bewijzen dan mensen?}
%\bigskip
\medskip
\adviwait

\begin{tabular}{rl}
Robbins, 1933: & is iedere \green{Robbins algebra} een \green{Boole algebra}? \\
\adviwait
\textbf{eqp}, 1996: & \textbf{ja$\,$!} \\
\noalign{\vspace{-\smallskipamount}}
& acht dagen computertijd
\end{tabular}
\medskip
\adviwait

{\'e\'e}n van de weinige bewijzen het eerst gevonden door een computer \\
niet erg conceptueel: probeert gewoon heel veel mogelijkheden

%\vfill
%\end{slide}
%
%\begin{slide}
%\slidetitle{onbeslisbaarheid}
%Turing, 1936:
%\begin{center}
%\red{het is onmogelijk een computerprogramma te maken \\ dat elk wiskundig probleem aankan}
%\bigskip
%\end{center}
%\adviwait
%
%in de praktijk is dit resultaat geen probleem:
%\begin{center}
%\green{mensen kunnen dat immers ook niet}
%\end{center}
%\adviwait
%
%maar er is helaas ook een echt probleem:
%\begin{center}
%\green{huidige stellingenbewijzers kunnen hele simpele \\ stellingen al niet bewijzen}
%\end{center}
\bigskip
\adviwait

\red{{interessant onderzoek, maar momenteel niet relevant voor de wiskunde}}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{bewijscheckers}
\slidetitle{de pentium bug}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/dagen/pics/pentium.eps}}
\vss
}
pentium: intel processor
\medskip
\adviwait

midden 1994: processor maakt rekenfouten \\
\red{FDIV bug}, niet genoeg precisie
\medskip

$\sf {5505001\over 294911} = 18.66665197$\dots\quad\green{(wiskunde)}

$\sf {5505001\over 294911} = 18.66600093$\dots\quad\green{(pentium)}
\medskip
\adviwait

pentium processor met bug wordt gratis vervangen \\
\red{schatting schade: 475 miljoen dollar}
\medskip
\adviwait

Harrison: werkt voor intel \\
bewijst full time met de \textbf{HOL} bewijschecker \blue{micro programma's} correct

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

\begin{slide}
\slidetitle{de metro en de B methode}
\vspace{-\bigskipamount}
\vbox to 0pt{
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/dagen/pics/meteor6.eps}}
\vss
}
1998: metro zonder bestuurder \\
\red{m{\'e}t{\'e}or} = \red{m{\'e}tro est-ouest rapide}

lijn 14 van de metro in Parijs \\
madeleine $\leftrightarrow$ biblioth{\`e}que nationale
\bigskip\medskip
\adviwait

systeem voor de besturing\\
\red{sacem} = \red{syst{\`e}me d'aide {\`a} la conduite, {\`a} l'exploitation et {\`a} la maintenance$\hspace{-1em}$}

geprogrammeerd in de programmeertaal ada
\bigskip
\adviwait

veiligheid van sacem \green{bewezen} met de \textbf{B methode} \\
\blue{commerci\"ele bewijschecker}

\vfill
\end{slide}

%\begin{slide}
%\slidetitle{de vier kleuren stelling}
%Guthrie, 1852: \\
%\red{kan iedere landkaart met maar vier kleuren zo worden ingekleurd \\
%dat aangrenzende landen nergens dezelfde kleur hebben?}
%\medskip
%
%Appel \& Haken, 1976:\quad \textbf{ja$\,$!}
%\bigskip
%\adviwait
%
%bewijs: bevat groot en onbegrijpelijk programma \\
%\green{bekijkt heel erg veel gevallen}
%
%50 dagen computertijd \\
%\adviwait
%(tegenwoordig: drie kwartier)
%
%\vfill
%\end{slide}

\begin{slide}
\slidetitle{het vermoeden van Kepler}
\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 de \textbf{sinaasappelstapeling} de efficientste \\
manier om bollen op te stapelen?}
\medskip
\adviwait

Hales, 1998:\quad \textbf{ja$\,$!}
\medskip
\adviwait

bewijs: bevat groot en onbegrijpelijk programma \\
\green{bekijkt heel veel gevallen} \\
3 gigabytes programma's/data +
paar maanden computertijd
\medskip
\adviwait

referees zeggen \red{99\% zeker} te zijn dat het klopt
\bigskip
\adviwait

\textbf{flyspeck project} \\
\blue{`formal proof of Kepler'}

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

\begin{slide}
\slidetitle{mizar}
bewijschecker uit Polen

Trybulec \\
\dashskip 1973: eerste idee\"en \\
\dashskip vandaag: \red{grootste wiskunde bewijscheck project ter wereld}
\medskip

anderhalf miljoen regels gecodeerde wiskunde \\
achthonderd \green{artikelen}
\bigskip

gebaseerd op de axiomatische verzamelingenleer \\
wiskundige \& leesbare bewijstaal

\vfill
\end{slide}

\begin{slide}
\slidetitle{hyperproof}
bewijschecken in de informatica \\
bewijschecken in de wiskunde \\
\textbf{bewijschecken in het onderwijs} \\
\adviwait
\dashskip \green{eerste orde predicatenlogica}
\bigskip
\adviwait

Barwise \& Etchemendy, 1994: \textbf{hyperproof}

eenvoudige redeneringen over een eenvoudige blokkenwereld \\
draait momenteel alleen op apple macintosh computers
\medskip

\red{redeneren in een diagram}

\vfill
\end{slide}

\begin{slide}
\adviembed{xvieww /home/freek/talks/dagen/pics/hyperproof.gif}\adviwait[1]%
\sectiontitle{voorbeeld van een checkbaar bewijs}
\slidetitle{Pythagore{\"\i}sche tripels}
een oplossing van
$$a^2 + b^2 = c^2$$
met $a$, $b$ en $c$ geen gemeenschappelijke delers, is altijd van de vorm
$$a = m^2 - n^2 \qquad b = 2mn \qquad c = m^2 + n^2\medskip$$
\textbf{voorbeelden}
$$\begin{array}{ccrcrcr}
m = 2 \qquad n = 1 & \quad\to\quad & 3^2 & + & 4^2 & = & 5^2 \\
m = 3 \qquad n = 2 & \to & 5^2 & + & 12^2 & = & 13^2 \\
m = 4 \qquad n = 1 & \to & 15^2 & + & 8^2 & = & 17^2 \\
m = 4 \qquad n = 3 & \to & 7^2 & + & 24^2 & = & 25^2
\end{array}$$
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{mizar bewijs}
\begin{flushleft}
\verb|reserve a,b,c,m,n for Nat;|
\end{flushleft}
\begin{flushleft}
\verb|let a,b,c; assume a^2 + b^2 = c^2;|\\
\verb|assume a,b are_relative_prime;|\\
\adviwait
\verb|then a is odd or b is odd;|\adviwait\verb| assume a is odd;|
\adviwait
\end{flushleft}
\begin{flushleft}
\verb|ex m,n st a = m^2 - n^2 & b = 2*m*n & c = m^2 + n^2|\\
\verb|proof|\\
\adviwait
\verb| b is even; c is odd;|\\
\adviwait
\verb|X: (c + a)/2,(c - a)/2 are_relative_prime;|\\
\adviwait
\verb| ((c + a)/2)*((c - a)/2) = (c^2 - a^2)/4 .= (b/2)^2;|\\
\verb| then ((c + a)/2)*((c - a)/2) is square;|\\
\adviwait
\verb| then (c + a)/2 is square & (c - a)/2 is square by X;|\\
\verb| consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;|
\verb| take m,n;|\\
\end{flushleft}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{mizar bewijs (vervolg)}
\begin{flushleft}
\begin{color}{slidegray}
\verb| consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;|\\
\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}
\bigskip
\adviwait
dit is bijna het echte mizar bewijs, maar
\red{te kort door de bocht}
\begin{itemize}
\item[$\bullet$]
stappen zijn te groot
\item[$\bullet$]
verwijzingen tussen stappen ontbreken
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{het volledige bewijs (fragment)}
\begin{flushleft}
\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[slidered]{x6}
\adviplay[slidered]{x8}
\adviplay[slidered]{x11}
\adviplay[slidered]{x13}
\adviplay[slidered]{x24}
\adviplay[slidered]{x25}
\adviplay[slidered]{x27}
\adviwait
\adviplay[slidegreen]{x1}
\adviplay[slidegreen]{x3}
\adviplay[slidegreen]{x7}
\adviplay[slidegreen]{x7a}
\adviplay[slidegreen]{x10}
\adviplay[slidegreen]{x10a}
\adviplay[slidegreen]{x12}
\adviplay[slidegreen]{x12a}
\adviplay[slidegreen]{x14}
\adviplay[slidegreen]{x14a}
\adviplay[slidegreen]{x16}
\adviplay[slidegreen]{x16a}
\adviplay[slidegreen]{x19}
\adviplay[slidegreen]{x22}
\adviplay[slidegreen]{x26}
\adviplay[slidegreen]{x28}
\adviplay[slidegreen]{x30}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{waarom proofchecken?}
\slidetitle{wordt wiskunde nu eindelijk echt \textbf{wis}kunde?}
\begin{itemize}
\adviwait
\item[$\bullet$]
\red{bugs in de checker, kapotte hardware}
\adviwait

(in de praktijk geen probleem)
\end{itemize}
\medskip

de Bruijn kriterium: \green{eenvoudige checker}
\bigskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\red{defini{\"e}ren je definities wel wat je denkt dat ze defini{\"e}ren?}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{QED}
1994, anonieme groep wiskundigen \& informatici:
\begin{center}
\red{laten we alle wiskunde in de computer stoppen$\,$!}
\end{center}
\medskip

erg interessant \textbf{QED manifesto} \\
antwoorden op twaalf mogelijke tegenwerpingen
\bigskip
\adviwait

\green{tot nog toe nog een utopie}

\vfill
\end{slide}

\begin{slide}
\slidetitle{het leukste computerspel ter wereld}

\begin{center}
\begin{tabular}{rl}
\green{wiskunde:} & \green{spannend} \\
\adviwait
\green{programmeren:} & \green{spannend} \medskip\\
\adviwait
\red{bewijzen in de computer:} & \red{het beste van twee werelden}
\end{tabular}
\end{center}
\medskip

je hoeft niet alleen op je begrip te vertrouwen $\;\to\;$ de computer helpt$\,$! \\
je weet zeker dat wat je doet helemaal goed is $\;\to\;$ geen `bugs'$\,$!
\medskip
\adviwait

\blue{
\begin{center}
een stelling die nog niet helemaal bewezen is \\
= \\
een `level' van een computerspel dat nog niet is uitgespeeld
\end{center}
}

\vfill
\end{slide}

\end{document}