\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{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{1pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}
\def\adviembeddelay{1}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut het servetje van Hendrik Lenstra}

\green{Freek Wiedijk} \\
Radboud Universiteit Nijmegen
\smallskip

\red{Kaleidoscoop 2 gastcollege} \\
Universiteit Utrecht
\smallskip

{2009\hspace{3pt}03\hspace{3pt}12, 14\hspace{1pt}:\hspace{1.4pt}15}

\end{slide}

\begin{slide}
\sectiontitle{een krantenknipsel}
\slidetitle{`QED zegt de computer'}

artikel door Bennie Mols
\medskip

{\green{NRC Handelsblad}} \\
wetenschapsbijlage van zaterdag 31 januari 2009
\bigskip

\textbf{\red{bewijsverificatie} met de computer}
\begin{itemize}
\item[$\bullet$]
{`voorstander':} informaticus Freek Wiedijk

\item[$\bullet$]
{`tegenstander':} logicus Ulrich Kohlenbach

\item[$\bullet$]
{`neutraal':} wiskundige Hendrik Lenstra

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{%
\adviembed{xviewww /home/freek/talks/servetje/pics/nrc.jpg}\adviwait[\adviembeddelay]%
het servetje versus bewijsverificatie}

\begin{center}
\bigskip
\bigskip
\begin{tabular}{ccc}
\noalign{\vspace{-\smallskipamount}}
computer &$\hspace{3em}$& \advirecord{a9}{formules op} \\
\noalign{\vspace{-\smallskipamount}}
checkt gevallen && \advirecord{a10}{een servetje} \\
\noalign{\medskip}
\gray{\advirecord{a1}{$\updownarrow$}} && \red{\advirecord{a5}{$\updownarrow$}} \\
\noalign{\medskip}
\gray{\advirecord{a2}{bewijsverificatie}} && \red{\advirecord{a6}{bewijsverificatie}} \\
\noalign{\vspace{-\smallskipamount}}
\gray{\advirecord{a3}{in bewijsassistent}} && \red{\advirecord{a7}{in bewijsassistent}} \\
\noalign{\bigskip\bigskip}
\green{\advirecord{a4}{(computerassistentie)}} && \green{\advirecord{a8}{(menselijk bewijs)}}%
\adviplay{a9}%
\adviplay{a10}%
\adviwait%
\adviplay{a1}%
\adviplay{a2}%
\adviplay{a3}%
\adviwait%
\adviplay[slidegreen]{a4}%
\adviwait%
\adviplay[white]{a1}%
\adviplay[white]{a2}%
\adviplay[white]{a3}%
\adviplay[white]{a4}%
\adviplay{a9}%
\adviplay{a10}%
\adviplay[slidered]{a5}%
\adviplay[slidered]{a6}%
\adviplay[slidered]{a7}%
\adviwait
\adviplay[slidegreen]{a8}%
%\adviwait
%\\
%\noalign{\bigskip}
%&& \red{bewijsassistent als} \\
%\noalign{\vspace{-\smallskipamount}}
%&& \red{wiskundige tekstverwerker}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{eerste misverstand:} bewijzen met computersupport $\ne$ bewijsverificatie}

\blue{bewijsverificatie:}

\blue{meestal:} computer controleert \textsl{bestaand} bewijs
\medskip
\smallskip
\adviwait

computer \textsl{kan} ook bovenop een bewijsassistent gevallen checken
\adviwait
\bigskip
\bigskip

{\blue{Lenstra:} {\large`\green{ik weet nu n\'og niet wie gelijk heeft}'}}
\bigskip
\adviwait

als je met een bewijsassistent werkt kun je \red{zeker} zijn dat het klopt\exclspace!
\adviwait
\smallskip

\gray{(bovenop een bewijsassistent werken kost wel v\'e\'el meer werk$\;$\dots)}


\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{tweede misverstand:} computeralgebra $\ne$ bewijsverificatie}

\blue{computeralgebra:} {geen} bewijzen

\blue{bewijsverificatie:} \red{w\'el bewijzen}
\bigskip

\textbf{wereld van verschil\exclspace!}
\medskip
\smallskip

\green{computeralgebra geeft vaak `foute' antwoorden} \\
gebrek aan semantiek
\bigskip
\medskip
\adviwait

\blue{computeralgebra:} \red{niet-triviale antwoorden}

\blue{bewijsverificatie (tot nog toe):} eenvoudige wiskunde

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{derde misverstand:} traditionele wiskunde $\approx$ bewijsverificatie}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=10em]{/home/freek/talks/servetje/pics/iceberg.eps}\par
\vss}\vspace{-1.4em}

\blue{bewijsverificatie:}

\blue{voor mij:} \red{tekstverwerker} \white{\advirecord{b2}{\rlap{voor wiskunde}}}\red{\advirecord{b1}{\rlap{\dots}}} \\
\adviplay{b2}%
\adviwait
\adviplay[white]{b2}%
\adviplay[slidered]{b1}%
{{\dots} voor \green{traditionele} wiskunde}
\adviwait
\bigskip
\medskip

\textbf{mens:} \\ stappen die je in een artikel opschrijft
\medskip

\textbf{computer:} \\ stapjes `onder de bewustzijnsdrempel'
\bigskip
\bigskip
\adviwait

\green{computer moet zich vooral niet tegen het bewijs aan bemoeien\exclspace!}


\vfill
\end{slide}

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

\begin{itemize}
\item[$\bullet$]
bewijzen met computerberekeningen als onderdeel

\green{correctheid wordt niet gecheckt}
\medskip

\item[$\bullet$]
computeralgebra

\green{correctheid wordt niet gecheckt}
\medskip

\item[$\bullet$]
automatisch stellingenbewijzen

\green{computer kan dat (nog) helemaal niet\exclspace: alleen speelgoedwiskunde}
\medskip

\item[$\bullet$]
\red{bewijsverificatie}

\green{correctheid wordt gecheckt \& realistische wiskunde}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{twee servetjes uit mijn bureaulade}
\slidetitle{een `servetje' uit Japan}

Michael Beeson \\
San Jos\'e State University
\medskip

schets van het bewijs van de \red{stelling van Liouville}
\adviwait
\bigskip
\medskip

\green{in HOL syntax\exclspace:}
\smallskip
\begingroup
\def\\{\char`\\}
\begin{alltt}\small
!x. algebraic x
    ==> ?n c. c > &0 /\\
              !p q. ~(q = 0) ==> &p / &q = x \\/
                                 abs(x - &p / &q) > c / &q pow n\toolong
\end{alltt}
\endgroup


\vfill
\end{slide}

\begin{slide}
\slidetitle{%
\adviembed{xviewww /home/freek/talks/servetje/pics/servetje1.jpg}\adviwait[\adviembeddelay]%
nog een `servetje'}

\red{vergeten\exclspace:}
\begin{quote}
waar vandaan\exclspace? \\
door wie geschreven\exclspace? \\
waar ging het over\exclspace?
\end{quote}
\bigskip
\medskip
\adviwait

\green{ondergrens voor $\prod_{p\le m} p$ zo te zien\white{\rlap{$\,$\advirecord{i2}{?}}}}\green{\advirecord{i1}{, maar waarvoor diende dat dan\exclspace?}}

$$\green{{{2^m\over (m + 1)\, m^{\sqrt{m}}}}\, \le \,\textstyle\prod_{p\le m} p}$$
\adviplay[slidegreen]{i2}
\adviwait
\adviplay[white]{i2}
\adviplay[slidegreen]{i1}

\vfill
\end{slide}

\begin{slide}
\slidetitle{%
\adviembed{xviewww /home/freek/talks/servetje/pics/servetje2.jpg}\adviwait[\adviembeddelay]%
wat staat er zoal op servetjes?}

\begin{itemize}
\item[$\bullet$]
{vergelijkingen}/ongelijkheden

\item[$\bullet$]
simpele uitspraken
\adviwait

\item[$\bullet$]
\red{geen} lopende tekst\exclspace!
\adviwait

wel af en toe een enkel woord
\begin{quote}
`\green{of degree $n$}' \\
`\green{if}' \\
`\green{QED.}'
\end{quote}
\adviwait

\item[$\bullet$]
\red{ge\"{\i}tereerde} vergelijkingen/ongelijkheden
$$\textstyle{2^m \mathrel{\red{=}} \sum_{i = 0}^m {m\choose i} \mathrel{\red{\le}} (m + 1) m^{\sqrt{m}}\cdot \prod_{p\le m} p}\adviwait$$

\item[$\bullet$]
{diagrammen}

\end{itemize}

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

\begin{slide}
\sectiontitle{bewijzen als doolhoven}
\slidetitle{procedurele versus declaratieve bewijzen}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\begin{picture}(5,5)
\put(0.5,4.5){\makebox(0,0){\white{\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,4.5){\makebox(0,0){\white{\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,4.5){\makebox(0,0){\white{\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,4.5){\makebox(0,0){\white{\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,3.5){\makebox(0,0){\white{\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,3.5){\makebox(0,0){\white{\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,3.5){\makebox(0,0){\white{\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,3.5){\makebox(0,0){\white{\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,2.5){\makebox(0,0){\white{\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,1.5){\makebox(0,0){\white{\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,0.5){\makebox(0,0){\white{\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,0.5){\makebox(0,0){\white{\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,1.5){\makebox(0,0){\white{\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,1.5){\makebox(0,0){\white{\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,0.5){\makebox(0,0){\white{\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,0.5){\makebox(0,0){\white{\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}}%
\put(4.5,0.5){\makebox(0,0){\white{\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}}%
\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[black]{e0}
\end{picture}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[black]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[black]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[black]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[black]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[black]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[black]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[black]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[black]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[black]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[black]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[black]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[black]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[black]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[black]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[black]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[black]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[black]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[black]{e0}%

\begin{itemize}
\item[$\bullet$]
\textbf{procedurele} oplossing

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

HOL, Coq, Isabelle
\smallskip

\adviwait
\item[$\bullet$]
\textbf{declaratieve} oplossing

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

Mizar

\end{itemize}

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

\begin{slide}
\slidetitle{{gestructureerde bewijzen}: declaratieve bewijzen procedureel annoteren}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\begin{picture}(5,5)
\put(0.5,4.5){\makebox(0,0){\white{\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,4.5){\makebox(0,0){\white{\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,4.5){\makebox(0,0){\white{\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,4.5){\makebox(0,0){\white{\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,3.5){\makebox(0,0){\white{\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,3.5){\makebox(0,0){\white{\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,3.5){\makebox(0,0){\white{\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,3.5){\makebox(0,0){\white{\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,2.5){\makebox(0,0){\white{\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,1.5){\makebox(0,0){\white{\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,0.5){\makebox(0,0){\white{\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,0.5){\makebox(0,0){\white{\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,1.5){\makebox(0,0){\white{\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,1.5){\makebox(0,0){\white{\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,0.5){\makebox(0,0){\white{\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,0.5){\makebox(0,0){\white{\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}}%
\put(4.5,0.5){\makebox(0,0){\white{\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}}%
\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[black]{e0}
\end{picture}
\end{center}
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{gestructureerde} oplossing

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

Isabelle
\medskip
\adviwait

\blue{procedureel en declaratief door elkaar gemengd}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{`formal proof sketches'}: declaratieve bewijzen indikken}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\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}}%
\put(.5,4.5){\red{\advirecord{f8}{\vector(1,0){3}}}}%
\put(3.5,4.5){\red{\advirecord{f9}{\vector(-3,-4){3}}}}%
\put(.5,.5){\red{\advirecord{f10}{\vector(1,0){4}}}}%
}
\adviplay[black]{e0}
\end{picture}
\end{center}
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\white{\advirecord{f1}{\strut\rlap{\textbf{declaratieve} oplossing}}}\advirecord{f2}{\textbf{`formal proof sketch'}}\adviplay{f1}

\begingroup
\white{%
\scriptsize
\advirecord{f6}{%
\strut\rlap{(0,0)
\advirecord{f3}{(1,0)
(2,0)}
(3,0)
\advirecord{f4}{(3,1)
(2,1)
(1,1)
(0,1)
(0,2)
(0,3)}
(0,4)
\advirecord{f5}{(1,4)
(1,3)
(2,3)
(2,4)
(3,4)}
(4,4)\toolong}}}%
\rlap{\advirecord{f7}{\red{{\small (0,0) (3,0) (0,4) (4,4)}}}}%
\adviplay[slidered]{f6}
\adviplay[slidered]{f3}
\adviplay[slidered]{f4}
\adviplay[slidered]{f5}
\adviwait
\adviplay[slidered]{f8}
\adviplay[slidered]{f9}
\adviplay[slidered]{f10}
\adviwait
\adviplay[white]{f3}
\adviplay[white]{f4}
\adviplay[white]{f5}
\adviwait
\adviplay[white]{f6}
\adviplay[slidered]{f7}
\adviwait
\adviplay[white]{f1}
\adviplay{f2}
\endgroup

\end{itemize}

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

\begin{slide}
\slidetitle{van traditioneel bewijs$\;$\dots}
Hardy \& Wright, \green{An Introduction to the Theory of Numbers}%: \textbf{7 lines}
\bigskip

\vbox to 0pt{
\vspace{-1.2\bigskipamount}
\begin{quote}
\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
\end{quote}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots}$\;$tot formal proof sketch$\;$\dots}
\green{precies hetzelfde in Mizar syntax}
\bigskip

\vbox to 0pt{
\vspace{-1\bigskipamount}
\begin{quote}\small
\white{\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{{\dots}$\;$tot formalisatie}
\green{completeren tot volledig Mizar bewijs}
\medskip
\smallskip

\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{;}}\\
\gray{\textbf{::} \textbf{lees verder in de volgende kolom}}
\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}
\vspace{-5pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{completeerbare formele bewijzen}
formal proof sketch = \textbf{alleen} `inference errors'
\adviwait
\smallskip

completeerbaar tot een volledig Mizar bewijs door toe te voegen:
\begin{itemize}
\item[$\bullet$]
\textbf{stappen} %\\
\item[$\bullet$]
\textbf{labels/referenties} %\\
\end{itemize}
\adviwait
\medskip
\smallskip

\red{formal} proof sketches \\
%\adviwait
correctheid: half-beslisbaar
\adviwait
\bigskip
\medskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{center}
\begin{picture}(300,50)
\put(40,24){\makebox(0,0){geen bewijs}}
\put(40,10){\line(0,1){8}}
\white{\advirecord{f1b}{\put(165,10){\line(0,1){8}}}%
\advirecord{f2b}{\put(40,14){\line(1,0){125}}}%
\advirecord{f3b}{\put(165,24){\makebox(0,0){volledig bewijs}}}}%
\advirecord{f1a}{\put(260,10){\line(0,1){8}}}%
\advirecord{f2a}{\put(40,14){\line(1,0){220}}}%
\advirecord{f3a}{\put(260,24){\makebox(0,0){volledig bewijs}}}%
\put(150,0){\makebox(0,0){\blue{formal proof sketch spectrum}}}
\advirecord{fx1}{\green{\put(120,31){\vector(0,-1){17}}}}
\advirecord{fx2}{\put(120,49){\makebox(0,0){\green{formal proof sketch}}}}%
\advirecord{fx3}{\put(120,38){\makebox(0,0){\green{op menselijk niveau}}}}%
\end{picture}
\end{center}
\adviplay{f1a}\adviplay{f2a}\adviplay{f3a}
\adviwait
\adviplay{fx1}\adviplay{fx2}\adviplay{fx3}
\adviwait
\adviplay[white]{f1a}\adviplay[white]{f2a}\adviplay[white]{f3a}
\adviplay{f1b}\adviplay{f2b}\adviplay{f3b}
\vss}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{bewijsassistenten voor wiskundigen: zes idee\"en}
\slidetitle{wiskunde versus informatica}

\begin{itemize}
\item[$\bullet$]
meeste bewijsassistenten ontwikkeld voor \textbf{informatica}

\green{verificatie van software} \\
\green{verificatie van hardware} \\
\green{verificatie van communicatieprotocollen} \\
\green{verificatie van `security' van systemen}
\vspace{1.25\smallskipamount}
\adviwait

\textbf{HOL, Coq, Isabelle, \dots} \\
\red{niet gemaakt door of voor wiskundigen}
\adviwait
\medskip

\item[$\bullet$]
\textbf{Mizar} \blue{is} gemaakt voor \textbf{wiskunde}, maar$\;$\dots
\smallskip

\red{niet automatiseerbaar door de gebruiker} \\
{je moet \textsl{alle} details zelf uitwerken}

\end{itemize}

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

\begin{slide}
\slidetitle{\textbf{idee 1\exclspace:} computerbewijzen door klikken en slepen}

\green{`proof by pointing'}
\smallskip

voorbeelden:
\begin{itemize}
\item[$\bullet$]
CtCoq \& PCoq = interfaces voor Coq

\item[$\bullet$]
atelier B
\end{itemize}
\adviwait
\bigskip

\blue{formaliseren $\approx$ programmeren}
\smallskip

programmeren door klikken en slepen niet praktisch
\adviwait

\vfill
\red{\textbf{geen goed idee}}
\end{slide}

\begin{slide}
\slidetitle{\textbf{idee 2\exclspace:} computerbewijzen in natuurlijke taal}

\green{inputtaal voor bewijsassistent: natuurlijke taal in {\LaTeX} syntax}
\adviwait

\begin{itemize}
\item[$\bullet$]
natuurlijke taal acceptabel parseren erg moeilijk
\adviwait

\item[$\bullet$]
natuurlijke taal erg ambigu
\adviwait

\end{itemize}
\bigskip
\medskip

\blue{formaliseren $\approx$ programmeren}
\smallskip

\green{programmeren in natuurlijke taal = COBOL}
\adviwait

\vfill
\red{\textbf{geen goed idee}}
\end{slide}

\begin{slide}
\slidetitle{\textbf{idee 3\exclspace:} declaratieve computerbewijzen}

\begin{itemize}
\item[$\bullet$]
veel meer controle over het bewijsproces

\item[$\bullet$]
formal proof sketches mogelijk

\item[$\bullet$]
minder systeemspecifiek \\ meer `portable'

\end{itemize}
\adviwait
\bigskip

\green{experts in bewijsverificatie\exclspace: declaratieve bewijzen \textbf{slecht} idee}

\blue{Georges Gonthier (= formalisator van de vierkleurenstelling in Coq)}
\adviwait

\vfill
\red{\textbf{toch} goed idee}
\end{slide}

\begin{slide}
\slidetitle{\textbf{idee 4\exclspace:} formele formules in een vorm dichterbij die van computeralgebra}
\begin{itemize}
\item[$\bullet$]
traditionele notatie\rlap{\exclspace:}
$$\green{\int {1\over x}\,dx = \ln |x| + C}\adviwait\smallskip$$

\item[$\bullet$]
computeralgebra (Mathematica)\exclspace:
\begin{center}
\smallskip
\texttt{\green{Integrate[1/x, x] = Log[x]}}
\smallskip
\end{center}
\adviwait

\item[$\bullet$]
bewijsassistent (Coq)\exclspace:
\begingroup
\smallskip
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\small
  \green{forall (a:IR) (Ha:Zero[<]a),
    \{c : IR | Feq (openl Zero) (([-S-] log_defn_lemma) a Ha)
    (Logarithm\{+\}[-C-]c)\}}
\end{alltt}
\endgroup

\end{itemize}
\adviwait

\vfill
\red{\textbf{goed idee\exclspace:} formules zoveel mogelijk in computeralgebra-stijl}
\end{slide}

\begin{slide}
\slidetitle{\textbf{idee 5\exclspace:} computer niet-triviale stappen laten nemen}

twee concurrerende mentale modellen:
\begin{itemize}
\item[$\bullet$]
bewijsassistent als \blue{tekstverwerker}

\item[$\bullet$]
bewijsassistent als \blue{research assistent}

\end{itemize}
\adviwait
\bigskip
\medskip

tweede model duidt op grondig onbegrip van wat een computer kan\toolong
\medskip

\green{kunstmatige intelligentie} voor wiskunde bestaat \white{\advirecord{h1}{\rlap{niet}}\advirecord{h2}{\rlap{nog {niet}}}}\red{\advirecord{h3}{niet binnen afzienbare~tijd\toolong}}
\adviplay[slidered]{h1}
\adviwait
\adviplay[white]{h1}
\adviplay[slidered]{h2}
\adviwait
\adviplay[white]{h2}
\adviplay[slidered]{h3}
\adviwait

\vfill
\red{\textbf{geen goed idee}}
\end{slide}

\begin{slide}
\slidetitle{\textbf{idee 6\exclspace:} automatisering van middelbare schoolwiskunde}

bewijsstappen:
\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*}
\bigskip
\adviwait

\green{verificatie met huidige technologie: heleboel werk}
\adviwait

\vfill
\red{\textbf{goed idee}\exclspace: dit soort stappen automatiseren}
\end{slide}

\begin{slide}
\sectiontitle{ge\"{\i}nteresseerd?}
\slidetitle{afstuderen op bewijsverificatie?}
\vspace{1em}
\begin{center}
\green{bachelor's scriptie} \\ stelling + bewijs%
\smallskip
\adviwait

$\blue{\downarrow}$
\smallskip

\green{master's scriptie} \\ \red{formalisatie}
van diezelfde wiskunde\rlap{\exclspace?}
\end{center}

\vfill
\end{slide}

\end{document}