\documentclass{article}
\usepackage[dutch]{babel}
\pagestyle{empty}
\raggedbottom

\begin{document}
\title{De kunst van het bewijzen}
\author{Freek Wiedijk}
\date{}
\maketitle

In de geschiedenis van de wiskunde zijn er drie revoluties
geweest:

\begin{itemize}
\item
De eerste revolutie was de ontwikkeling van \textbf{bewijzen}
in de Griekse oudheid.
V\'o\'or deze revolutie bestond wiskunde voornamelijk uit
\emph{berekeningen} (waarbij we het {oplossen van een vergelijking}
ook als een vorm van het berekenen van een antwoord zien.)
Bij berekenen gaat het om het \emph{wat} van een antwoord,
terwijl het bij bewijzen om het \emph{waarom} van dat
antwoord gaat.
Deze Griekse ontwikkeling vond zijn hoogtepunt in \emph{De
Elementen} van Euclides, een boek waarin -- bewijs na bewijs --
de meetkunde systematisch wordt ontwikkeld.

\item
De tweede revolutie was de ontwikkeling van \textbf{rigor}
aan het eind van de negentiende eeuw.
Daarvoor was wiskunde niet volledig precies.
Zo rammelt Euclides' ontwikkeling van de meetkunde als je
er met moderne ogen naar kijkt, en
ook de ontwikkeling van de infinitesimaalrekening
door Isaac Newton en Gottfried Leibniz was niet rigoureus, met referenties
naar oneindig kleine grootheden.
Eind negentiende eeuw kwam hieraan een eind met de ontwikkeling
van $\epsilon$/$\delta$ definities van limieten door Augustin Louis Cauchy.
Deze ontwikkeling culmineerde in de verzamelingenleer van Georg Cantor
en de ontwikkeling van de mathematische logica door Gottlob Frege.

De meetkunde van Euclides werd voor het eerst rigoureus gemaakt
rond de eeuwwisseling door David Hilbert.
Een bijzonder fraaie variant hierop werd later ontwikkeld door
Alfred Tarski.

\item
De derde revolutie is de ontwikkeling van praktische \textbf{formele} wiskunde.
Hierbij wordt wiskunde in de computer gerepresenteerd op een manier
dat \emph{alle} details in de computer aanwezig zijn.
De computer kan hierdoor de correctheid van de wiskunde volledig mechanisch
nagaan.
Bij rigoureuze wiskunde is het \emph{in principe} mogelijk om bewijzen
volledig precies op te schrijven, maar bij formele wiskunde wordt
dit ook \emph{in de praktijk} gedaan.
Deze derde revolutie vindt momenteel plaats.
Ze begon eind jaren zestig in Eindhoven met de ontwikkeling van het Automath
systeem door professor N.G.~de~Bruijn, en heeft daarna een hoge vlucht genomen.

\end{itemize}

\noindent
Er zal een presentatie geven worden van de huidige toestand van
formele wiskunde.

Ten eerste zal formele wiskunde worden afgezet tegen andere vormen van
wiskunde in de computer: rigoureuze numerieke methoden, computer algebra,
en automatisch stellingenbewijzen.

Vervolgens zullen de belangrijkste systemen die tegenwoordig
voor formele wiskunde bestaan de revue passeren:
het Engelse \textbf{HOL} systeem,
de Engels/Duit\-se opvolger hiervan genaamd \textbf{Isabelle}, het Franse \textbf{Coq} systeem, en het Poolse \textbf{Mizar} systeem.

Er zullen verschillende formele bewijzen in deze systemen worden
vertoond, zoals formele bewijzen van:
\begin{itemize}
\item
De hoofdstelling van de algebra (voor het eerst bewezen
door de `prins der wiskundigen' Carl Friedrich Gauss, in diens proefschrift uit 1799)
die zegt dat iedere niet-triviale polynomiale
vergelijking altijd een oplossing heeft in de complexe getallen.

\item
De priemgetalstelling als eerst bewezen door Jacques Hadamard en Charles Jean de la Val\-l\'ee-Poussin, die zegt dat het aantal priemgetallen kleiner
dan $n$ ongeveer $n\over\log n$ is als $n$ naar oneindig gaat,
in de zin dat de verhouding van deze twee grootheden naar $1$ gaat.
Het bewijs van deze stelling maakt gebruik van de locatie in het complexe vlak
van de nulpunten van de $\zeta$ functie van Bernhard Riemann,
waarover ook de fameuze \emph{Riemann-hypothese} gaat.

\item
De stelling van Camille Jordan (ondanks de naam bewezen door Oswald Veblen) die zegt dat een gesloten continue kromme die
zichzelf niet doorsnijdt het platte
vlak in precies twee delen verdeelt: een binnenkant en een buitenkant.
Dit is een stelling uit de topologie, een vakgebied dat werd ontwikkeld
door onze landgenoot L.E.J.~Brouwer.

\item
De eerste onvolledigheidsstelling van Kurt G\"odel, die zegt dat er voor
ieder axiomasysteem ware uitspraken bestaan die niet 
uit die axioma's te bewijzen zijn (de zogenaamde \emph{G\"odel-zin}).

\item
De vierkleurenstelling, die zegt dat een landkaart altijd met vier
kleuren is te kleuren op een manier dat aangrenzende landen steeds verschillende
kleuren hebben.
Aan de correctheid van het bewijs van deze stelling door Kenneth Appel en Wolfgang Haken
uit 1976 werd lange tijd getwijfeld,
omdat er bij het bewijs grote computerberekeningen waren gebruikt.
Maar nu dit bewijs is geformaliseerd is het zeker dat het bewijs klopt.

\end{itemize}

\noindent
Tenslotte zal een eenvoudiger voorbeeld van een formeel bewijs
in meer detail worden gepresenteerd.
Het gaat hierbij om een formule die \emph{Pythagore\"\i sche
drietallen} genereert.
Dit zijn drietallen van gehele getallen $(a,b,c)$ met $a^2 + b^2 = c^2$,
die dus met rechthoekige driehoeken met geheeltallige
zijden corresponderen.
Er zal worden getoond hoe met het Mizar-systeem kan worden bewezen
dat alle Pythagore\"\i sche drietallen door de gegeven formule
worden gegenereerd.

\end{document}

\section*{Mogelijke plaatjes}
\begin{itemize}
\item
Hoofden van wiskundigen:
\begin{itemize}
\item \textbf{Euclides}
\item Newton
\item Leibniz
\item Cauchy
\item Cantor
\item Frege
\item Hilbert
\item Tarski
\item \textbf{de Bruijn}
\item Gauss
\item Hadamard
\item de la Vall\'ee Poussin
\item Riemann
\item Jordan (is daar een plaatje van te vinden?)
\item Veblen (is daar een plaatje van te vinden?)
\item Brouwer
\item G\"odel
\item Appel \& Haken (is daar een plaatje van te vinden?)
\item Pythagoras
\end{itemize}

\item
Diagrammen bij traditionele bewijzen:
\begin{itemize}
\item \textbf{stelling van Pythagoras uit Euclides}
\item $\epsilon$/$\delta$ definitie
\item diagram uit boek over Tarski's versie van de meetkunde
\item priemgetalstelling (is daar een geschikt diagram van te vinden?)
\item Jordan stelling
\item vierkleurenstelling
\end{itemize}

\item
Fragmenten van geformaliseerde bewijzen:
\begin{itemize}
\item {HOL bewijs van priemgetalstelling}
\item Coq bewijs van vierkleurenstelling
\item Mizar bewijs van Jordan stelling
\item \textbf{Mizar bewijs over Pythagore\"\i sche drietallen}
\item misschien: visueel interessanter ander Mizar bewijs
\end{itemize}

\end{itemize}