\documentclass{article}
\usepackage[dutch]{babel}
\usepackage[top=1in,bottom=1in,left=1in,right=1in]{geometry}
\usepackage{multicol}
\raggedbottom
\begin{document}
\tolerance=400

\begin{multicols}{2}
\parindent=0em
\parskip=0pt
\parfillskip=1em plus 1fil

\textbf{\large HOL, ML}
\vspace{1.2em}

Sinds een tiental jaren hou ik me intensief bezig
met het onderwerp `bewijsassistenten'.

Bewijsassistenten zijn programma's waarmee
wiskunde door de computer op correctheid kan worden
gecontroleerd.
Dat wil zeggen: mits op de juiste wijze gecodeerd.
Zulke gecodeerde wiskunde heet `een formalisatie'
en ziet er in de huidige systemen uit als volslagen
onbegrijpelijke computercode.
Er zijn vandaag de dag een viertal bewijsassistenten waarmee
serieus wiskunde `geformaliseerd' wordt:
Mizar, HOL, Isabelle en Coq.
Mijn onderzoeksterrein is het ontwikkelen van technologie
om deze systemen \emph{beter} te maken.

Er zijn nog niet veel hedendaagse wiskundigen die een helder beeld van
bewijsassistenten hebben.
Laat ik daarom eerst een tweetal misverstanden over bewijsassistenten uit de weg ruimen.
Ten eerste worden bewijsassistenten \emph{niet} gebruikt om
de wiskunde verder te helpen, om nieuwe resultaten te bereiken.
Je mag al blij zijn als je wiskunde die je door en door begrijpt
met een heleboel werk voor een bewijsassistent verteerbaar kunt maken.
Ten tweede zijn bewijsassistenten iets totaal anders dan
systemen voor computer algebra en ook iets totaal anders dan automatische stellingenbewijzers.
Deze drie soorten software hebben momenteel niets
met elkaar te maken.

Het \emph{aardige} van bewijsassistenten is dat als je je wiskunde
eenmaal `geformaliseerd' hebt, en het systeem zegt dat het klopt, dat je
dan ook \emph{volkomen} zeker kan zijn
dat het inderdaad klopt.
Over hoe zeker dat `volkomen zeker' is kun je een hoop woorden
vuil maken, maar laten we zeggen: een heel stuk zekerder dan op
welke andere wijze dan ook bereikbaar is.
De \emph{enige} ruimte voor `fouten' bij formalisatie
is dat je denkt dat er wat anders staat dan er staat,
dus dat je intu\"{\i}tieve begrip niet overeenkomt met wat je in werkelijkheid
hebt gedefinieerd en bewezen.
Maar \emph{wat} er staat is zo zeker als wat.
%
En dat heeft iets heel moois.
Een formalisatie is als een volkomen feilloze diamant.

Twee van de meest indrukwekkende formalisaties die ik ken
zijn allebei gemaakt door John Harrison.
Voor deze formalisaties gebruikte hij de mooiste
van de vier bovengenoemde bewijsassistenten, zijn eigen
versie van het HOL systeem.
In zijn werk bij Intel gebruikt hij dit om floating
point processors correct te bewijzen.
Formalisatie van wiskunde doet hij er in zijn vrije tijd bij,
voor de aardigheid.

De eerste van deze formalisaties bewijst de correctheid van de \emph{kernel}
van zijn HOL systeem.
Het laat zien dat je er zeker van kan zijn dat dit programma geen `bugs' bevat
waardoor per ongeluk incorrecte bewijzen als correct worden geaccepteerd.
Nu kun je morren dat hier een kip en ei probleem is
(de checker kan fout zijn en daarom de formalisatie accepteren terwijl die
niet klopt),
of over hoe het dan zit met G\"odels tweede onvolledigheidsstelling, maar dat zijn bezwaren die
geen hout snijden.
Wat wel een serieus bezwaar is, is dat de formalisatie momenteel alleen
het `moeilijke' stuk van de HOL kernel behandelt (het deel dat te maken
heeft met het hernoemen van variabelen bij substitutie).
%Het is dus niet af, in zekere zin.
%Momenteel heb ik bij NWO een aanvraag lopen voor een promovendus
%om dit af te maken.
Als evenwel binnenkort de \emph{hele} HOL kernel correct
bewezen is, zal er een heel interessant punt bereikt zijn!

De tweede formalisatie is een vertaling van het bewijs
van de priemgetalstelling uit de analytische getaltheorie.
Hierbij wordt door beschouwing van de nulpunten van
de Riemann zeta-functie bewezen dat de verhouding tussen het aantal priemgetallen
$\le n$ en $n/\ln n$ in de limiet van $n$ naar oneindig gelijk is aan
\'e\'en.
Het analytische bewijs van deze stelling was een paar jaar geleden door
de verzamelingstheoreticus Bob Solovay als uitdaging aan de bewijsassistentengemeenschap gegeven.
Zijn verwachting was dat het nog decennia zou duren voor de technologie
zo ver zou zijn dat dit bewijs in de praktijk geformaliseerd kon worden.
Maar toen kwam John Harrison die in \'e\'en maand tijd, naast zijn gewone werk bij Intel,
een bestand van 4.314 regels HOL code produceerde waarin hij een
vijftal pagina's uit een boek van Donald J. Newman formaliseerde.
(Die HOL code blijkt ongeveer \emph{acht} keer zo groot als de {\LaTeX}
van Newmans bewijs: dit heet de \emph{de Bruijn factor}.)
Hij deed dit voor het \emph{Festschrift} voor zijn promotor die dat
jaar zestig was geworden.
Het controleren van deze formalisatie
-- inclusief het checken van alle gebruikte basiswiskunde --
kost de computer
ongeveer twintig minuten.
Gedurende die tijd construeert het HOL systeem een gerichte acyclische graaf met 22.882.354 
punten, die loopt van drie beginpunten voor de drie axioma's van het HOL systeem aan de ene kant,
naar een eindpunt dat correspondeert met de priemgetalstelling.

De reden dat John Harrison dergelijke indrukwekkende dingen met zijn HOL
systeem kan doen is omdat hij \'e\'en van de beste \emph{bibliotheken}
van geformaliseerde wiskunde heeft die er zijn.
Het is een aantrekkelijke gedachte (een soort wiskundige versie van
het `human genome-project') om een dergelijke bibliotheek te maken
voor \emph{alle} wiskunde die je als algemeen ontwikkeld wiskundige hoort te
kennen.
Dat is dus ongeveer de wiskunde die vroeger in het kandidaats- en nu in het bachelors-programma wordt behandeld.
Ik heb ooit uitgerekend dat het ongeveer 140 man-jaar zal kosten om dat
allemaal te formaliseren.
Een interessante dagdroom is om je af te vragen of dat er ooit van zal komen.
En zo ja: wanneer dan, en in welke vorm.

\end{multicols}

\end{document}