\let\polishl=\l

\documentclass{article}
\usepackage{amssymb,url,alltt,bk0,bk1}
\raggedbottom
\usepackage[dutch]{babel}
\usepackage{graphicx,alltt}

\def\toolong{$\hspace{-10em}$}
\newcommand\real{{\mathbb R}}
\newcommand\rat{{\mathbb Q}}
\newcommand\complex{{\mathbb C}}

\newtheorem{stelling}[definition]{Stelling}
\usepackage[square]{harvard}
\citationmode{full}

\begin{document}
\bibliographystyle{eb}

\title{Bewijzen: romantisch of \emph{cool}?}
\author{Henk Barendregt \& Freek Wiedijk}
\weg{Institute for Computing and Information Sciences \\
Radboud University Nijmegen \\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\maketitle

\begin{abstract} \noi Computers kunnen ons helpen wiskunde te doen 
door voor ons te rekenen, met getallen of symbolisch. Systemen
hiervoor zijn goed ontwikkeld. Er worden nu ook computersystemen
ontwikkeld, de zogenaamde wiskundige assistenten, die ons zelfs kunnen
helpen met het verifi\"eren en verder ontwikkelen van het vak. Het
menselijke vernuft zal hierdoor niet overbodig worden.
\end{abstract}

\section{De `wis' van wiskunde}
Eigenwijs? Dat wordt er wel over je beweerd als je van wiskunde
houdt. Het onderwerp houdt zich bezig met die dingen waarvan je zeker
kunt zijn. In andere talen heet het vak \emph{mathematics,
math\'ematiques, mat\'ematica, $\ldots$ }. Het Nederlands heeft een
heel ander woord, hoewel `mathesis' vroeger ook wel gebruikt werd. De
stam `wis' is verwant aan `zeker', aan `weten'. En ja, het kan
eigenwijs overkomen als je je bezighoudt met deze zaken. Maar je weet
ook wel dat alleen sommige dingen zeker zijn: het weer kunnen we niet
op de lange termijn voorspellen. Maar dat weten we dan ook weer
zeker. Trouwens, wat de zekerheid betreft die de wiskunde je geeft,
het gaat niet om gelijk te krijgen, maar om gelijk te hebben!

Waar komt die zekerheid nu vandaan? Die is het gevolg van het
bewijzen.  Een uitspraak wordt onderzocht op al zijn mogelijke
aspecten. En als dat er oneindig veel zouden zijn, dan worden er
methoden ingevoerd om binnen eindige tijd al die oneindig vele
gevallen te kunnen behandelen: symbolisch redeneren (`met $x$ en $y$')
en inductie (een uitspraak is waar voor alle natuurlijke getallen als
die waar is voor 0 en als de waarheid voor $x$ die voor $x+1$ tot
gevolg heeft). Dat geeft de precisie, kracht en zekerheid van de
wiskunde die haar zo mooi (en voor sommigen: onuitstaanbaar) maakt.

Waarom geven bewijzen zekerheid? Dat komt omdat je alleen uitgaat van
de definities, van wat er gegeven\footnote{Er zijn ook axioma's, maar
die vormen een impliciete definitie van het onderwerp waarmee je je
bezig houdt. Zo is er voor de optelling in de natuurlijke getallen het
axioma $0+x=x$. Dit is in feite een afspraak: zo willen we optellen.}
is, en dan op grond van een sluitende redenatie een conclusie
trekt. Blijft de vraag wat een sluitende redenering is. Tijdens een
werkcollege vragen studenten vaak ``Mag ik deze stap maken?'' Het
antwoord van de docent is dan ``Als je in de eerste plaats jezelf en
daarna mij ervan kunt overtuigen dat deze juist is.'' Het
uiteindelijke oordeel van de logische en daarmee wiskundige
correctheid hangt af van een mentaal oordeel. Maar het bijbehorende
oordeelsvermogen moet wel getraind worden!

Nu kan het voorkomen dat een bewijs zeer lang is. Onze geest kan dan
moe worden bij de verificatie ervan en zo kunnen er foutjes binnen
sluipen. Stellingen met lange---en ook extreem lange---bewijzen komen
voor. Je kunt zelfs aantonen dat er altijd nieuwe stellingen zullen
zijn met alleen extreem lange bewijzen (en een relatief korte
formulering). Dit treedt onder andere, maar niet uitsluitend, op als
lange berekeningen onderdeel vormen van het bewijs, zoals bij de vier
kleurenstelling. Om deze redenen heeft de Nederlandse wiskundige Dick
de Bruijn (geboren 1918) een taal Automath ontwikkeld waarin een
bewijs zodanig in stapjes uit gesplitst kan worden dat een computer
met een eenvoudig programma het kan verifi\"eren op fouten en foutjes,
zie \ncite{automath}.  Wij hoeven slechts \'e\'enmaal na te gaan of
het computerprogramma correct is (het uiteindelijke menselijke oordeel
blijft) en dan kunnen we op deze manier de hoogst mogelijke graad van
zekerheid verkrijgen. Wel moeten de bewijzen dan \emph{geformaliseerd}
worden, dat wil zeggen van alle mogelijke details voorzien worden
klaar voor de verificatie door de computer. Op interactieve wijze,
door samenwerking tussen wiskundige en computer komen volledig
geformaliseerde bewijzen tot stand en worden ze nagekeken. Op deze
wijze resulteert wat we noemen \emph{Computer Wiskunde}. We geven twee
voorbeelden.\\

\includegraphics[height=5cm,width=10cm]{plaatje.eps}

\section{Het bestaan van positieve irrationale
getallen met rationale macht} 
We geven nu een stelling en een bewijs
daarvan. De uitspraak is op zichzelf niet erg interessant, maar er
moet een beetje geredeneerd en gerekend worden en dat illustreert de
methode van bewijsverificatie. Een re\"eel getal $r$ heet rationaal als 
het een breuk is, dus als
$r=\frac{p}{q}$ voor zekere gehele getallen $p,q$.
Anders heet het irrationaal.

\subsection*{Een romantisch bewijs}

\begin{stelling}\label{2.1}
Er bestaan positieve irrationale getallen $x$ en $y$ zodat hun macht
$x^y$ rationaal is. In symbolen $\exists
x,y\in(\real_{>0}\backslash\rat).x^y\in\rat$.
\end{stelling}
%\begin{proof}
{\sc Bewijs.} We weten dat $\sqrt{2}\in\real_{>0}\backslash\rat$. 

Geval 1. $\sqrt{2}^{\sqrt{2}}\in\rat$. Dan zijn we klaar: neem
$x=y=\sqrt{2}$.

Geval 2.  $\sqrt{2}^{\sqrt{2}}\notin\rat$. Neem dan
$x=\sqrt{2}^{\sqrt{2}}$ en $y=\sqrt{2}$. Dan zijn
$x,y\in(\real_{>0}\backslash\rat)$ en $x^y=(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}}=
\sqrt{2}^{\sqrt{2}\cdot\sqrt{2}}=\sqrt{2}^2=2\in\rat$.\qed\dwn Er valt
hier iets op. Hoewel we niet weten of $\sqrt{2}^{\sqrt{2}}$ rationaal
is of niet konden we toch inzien dat de stelling juist is. Als iemand
ons dan vraagt `Geef die getallen $x$ en $y$ dan eens', dan kunnen we
dat niet voor $x$. Dit komt omdat het bewijs niet
\emph{intu\ui{}tionistisch} geldig is. Met behulp van
intu\ui{}tionistische logica kun je alleen existentie uitspraken
bewijzen als je ook daadwerkelijk voorbeelden kunt geven. Met meer
moeite kan er toch een intu\ui{}tionistisch bewijs gegeven worden. Er
is de stelling van Gelfond-Schneider, die impliceert dat
$\sqrt{2}^{\sqrt{2}}\notin\rat$. Dat kan intu\ui{}tionistisch bewezen
worden en zo hebben we dan wel een konkreet voorbeeld voor bovenstaande
stelling: $x=\sqrt{2}^{\sqrt{2}},\, y=\sqrt{2}$.

Het bewijs van de stelling---we beperken ons tot de klassieke (niet
intu\ui{}tio\-nis\-ti\-sche) versie---is geheel duidelijk. We noemen het een
`romantisch' bewijs: begrijpelijk voor de menselijke geest.

\subsection*{Bewijzen via de computer: eerste poging}
We kunnen proberen het bewijs van de stelling \ref{2.1}
met behulp van een computer te leveren.
\subsubsection*{Numerieke berekeningen (GP/PARI calculator)}
Een goed numeriek programma zal niet blijken te helpen.
\begin{alltt}
? sqrt(2)
%1 = 1.414213562373095048801688724
? %1^%1
%2 = 1.632526919438152844773495381
? %2^%1
%3 = 1.999999999999999999999999999
\end{alltt}
Ook al zou het antwoord \cour{\%3 = 2.000000000000000000000000000} zijn, dan
kunnen we nog niet concluderen dat dit getal rationaal is.  En verder
is natuurlijk helemaal niet duidelijk dat er bij \cour{\%1} en
\cour{\%2} irrationale getallen staan.

\subsubsection*{Computeralgebra (Mathematica)}
Met behulp van `symbolisch rekenen' kunnen we iets meer. Een systeem
dat dit kan rekent $\sqrt{2}^{\sqrt{2}}$ exact uit.
\begin{alltt}
In[1]:= (Sqrt[2]^Sqrt[2])^Sqrt[2]\medskip
Out[1]= 2
\end{alltt}
We zouden het systeem kunnen leren dat $\frac{p}{q}$ en dus ook $2$
rationaal is. Maar weer kan er zelfs niet uitgedrukt worden dat
bijvoorbeeld $\sqrt{2}$ irrationaal is.

\subsection*{Bewijzen via de computer: \emph{cool}}
Alleen al het formuleren op een computer van onze stelling mislukte
boven.  Een numeriek programma kan wel $3.7-1.8=1.9$ uitrekenen, maar
niet $r-r$ als we niet vertellen wat $r$ is en daar dan 0 uit laten komen. In een programma voor
symbolisch rekenen kan dit laatste wel. Maar in zulke systemen kunnen
we weer geen eigenschappen zoals rationaliteit of de ontkenning
daarvan weergeven.

\subsubsection*{Interactieve bewijsverificatie (Mizar)}
Het systeem Mizar van Trybulec (Bia{\polishl}ystok, Polen, in ontwikkeling sinds 1974),
dat ge\ui{}nspireerd is door het werk
van de Bruijn, kan wel alle mogelijke wiskundige uitspraken doen. Dat
komt omdat de logica (en eveneens de verzamelingenleer) is ingebouwd
in dit systeem. Bewijzen zullen door de gebruiker moeten worden
ingevoerd, waarna ze volledig geverifieerd worden.

\begin{alltt}\footnotesize
---------------------------------------------------------------
theorem
 ex x, y st x is irrational & y is irrational & x^y is rational
proof
 set w = sqrt 2;
 w > 0 by SQUARE_1:84;
 then A1: (w^w)^w = w^(w*w) by POWER:38
  .= w^(w^2) by SQUARE_1:def 3
  .= w^(2) by SQUARE_1:def 4
  .= w^2 by POWER:53
  .= 2 by SQUARE_1:def 4;
 per cases;
 suppose A2: w^w is rational;
  take w, w;
  thus thesis by A2,IRRAT_1:1,INT_2:44;
 end;
 suppose A3: w^w is irrational;
  take w^w, w;
  thus thesis by A1,A3,IRRAT_1:1,INT_2:44;
 end;
end;
---------------------------------------------------------------
\end{alltt}
Gebruik wordt gemaakt van reeds eerder geverifieerde stellingen.\dwn
{\tt\footnotesize
\def\^{\char`^}
\btab{|l|l|}
\hline
POWER:38\hoog{1.2em}& a > 0 implies a to\_power b to\_power c = a to\_power (b * c);\dwn
POWER:53       & a to\_power 2 = a\^2;\dwn
SQUARE\_1:84   &  1 < sqrt 2;\dwn
SQUARE\_1:def 3&  x\^2 = x * x;\dwn
SQUARE\_1:def 4&  0 <= a implies 0 <= sqrt a \& (sqrt a)\^2 = a;\dwn
INT\_2:44      &  2 is prime;\dwn
IRRAT\_1:1     &  p is prime implies sqrt p is irrational;\dwn
\hline
\etab}\dwn
De bibliotheek van het systeem Mizar is behoorlijk groot. Zo'n 50.000
stellingen zijn er geformaliseerd en goed bevonden.
Voorbeelden van stellingen die in de Mizar bibliotheek voorkomen
zijn de
hoofdstelling van de algebra (ieder polynoom over $\complex$ heeft een
wortel in $\complex$); de hoofdstelling van de analyse (differenti\"eren
van de integraal van een continue functie $f$ levert $f$ zelf op);
de Brouwer dekpunt stelling (een continue functie van een bol naar
zichzelf heeft altijd een punt dat op zijn plaats blijft).

\subsubsection*{Automatische deductie (Otter)}
In tegenstelling tot Mizar zoekt het systeem Otter, ontwikkeld door
McCune (Argonne, Illinois, in ontwikkeling sinds 1988),
zelf naar bewijzen. Je moet dan wel een handje helpen en
bijvoorbeeld voorzeggen dat $\sqrt{2}$ irrationaal is. Omdat onze
stelling vrij eenvoudig is, kan het bewijs verder door Otter zelf
gevonden worden.  In het algemeen duurt het te lang om een computer
naar bewijzen te laten zoeken. Voor bovenstaande bewering---en met
menselijke hulp---kan dat dus wel. Het systeem Otter werkt met de
zogenaamde eerste orde predicatenlogica.  Naast termen zoals $x,y,x\x
y, x^y,\ldots$ en gelijkheden zoals $(x^y)^z=x^{y\x z}$ die ook al
gebruikt worden in systemen voor computeralgebra, heb je nu ook een
weergave voor de zogenaamde kwantoren ``er is een $x$'' en ``voor alle
$x$''. De manier waarop naar een bewijs gezocht wordt is de zogenaamde
\emph{resolutie methode}. Hierbij wordt geprobeerd met de resolutie
methode (een bepaald soort bewijs uit het ongerijmde) de stelling aan
te tonen. Het gegenereerde bewijs is meestal niet begrijpelijk, zie
het volgende voorbeeld.
%(Vb \verb+A->B&C, C->D, ~D |- ~A+ : via resolutie
%wordt dit onbegrijpelijk; wellicht eenvoudiger \verb+A->B, ~B |- ~A+).

\begin{alltt}\footnotesize
----------------------- Input --------------------------------------
set(auto).
op(300, xfy, ^).
formula_list(usable).
all x (x*x = x^2).
all x (sqrt(x)^2 = x).
all x y z ((x^y)^z = x^ (y*z)).
-rational(sqrt(2)).
rational(2).
end_of_list.
formula_list(sos).
-(exists x y (-rational(x) & -rational(y) & rational(x^y))).
end_of_list.
------------------------- PROOF -----------------------------------\medskip
1 [] -rational(sqrt(2)).
2 [] rational(x)|rational(y)| -rational(x^y).
3 [factor,2.1.2] rational(x)| -rational(x^x).
4 [] x*x=x^2.
6,5 [copy,4,flip.1] x^2=x*x.
7 [] sqrt(x)^2=x.
8 [copy,7,demod,6] sqrt(x)*sqrt(x)=x.
10 [] (x^y)^z=x^ (y*z).
12 [] rational(2).
22 [para_from,10.1.1,2.3.1] 
         rational(x^y)|rational(z)| -rational(x^ (y*z)).\toolong
58 [para_into,22.3.1.2,8.1.1] 
         rational(x^sqrt(y))|rational(sqrt(y))| -rational(x^y).\toolong
67 [para_into,58.3.1,5.1.1,unit_del,1] 
         rational(x^sqrt(2))| -rational(x*x).\toolong
84 [para_into,67.2.1,8.1.1] rational(sqrt(x)^sqrt(2))| -rational(x).
91 [hyper,84,12] rational(sqrt(2)^sqrt(2)).
96 [hyper,91,3] rational(sqrt(2)).
97 [binary,96.1,1.1] $F.\medskip 
----------------------- end of proof -------------------------------
\end{alltt}% $

Op een geheel andere manier---op grond van een door Collins \ncite{coll76}
en anderen verbeterd algoritme van Tarski \ncite{tars51} dat gebruikt maakt
van logische manipulaties die met name gelden voor bepaalde
structuren---kunnen bewijzen voor uitspraken uit de Euclidische
meetkunde automatisch gegenereerd worden, tenzij het systeem aangeeft
dat de uitspraak onjuist is. De efficientie van het algoritme is matig
en voor een overlappende verzameling van problemen is er het snellere
algoritme van Buchberger, see \ncite{buchwink98} en de methode van Wu,
see \ncite{chou88}.

\section{Hoe win je de hand van Portia?}
Vrij naar het toneelstuk ``de Koopman van Veneti\"e'' van Shakespeare heeft
\ncite{smul} de volgende puzzel verzonnen. 

\begin{quote}
\parindent=1em \noi De huwbare Portia heeft een gouden en een zilveren
kistje.  Zij kiest haar toekomstige echtgenoot uit niet op grond van
zijn kracht, maar op grond van zijn intelligentie. In een van de
kistjes plaatst ze een portret van haarzelf. Ze sluit de
kistjes. Leesbaar op het gouden kistje staat de inscriptie ``Het
portret zit niet in dit kistje''. Op het zilveren kistje staat
``Precies \'e\'en van deze twee uitspraken is waar''. Portia legde uit
aan een man die naar hand dong, dat de uitspraken waar of onwaar
kunnen zijn, maar dat als hij het kistje kan uitkiezen waar haar
portret in zit, zij met hem zal trouwen.
\end{quote}
Het probleem is nu om gebruik te maken van de inscripties, zonder dat
je weet of ze al dan niet waar zijn. De romantische oplossing is als
volgt. Stel de uitspraak op het zilveren kistje is waar. Dan is die op
het gouden kistje onwaar en dus zit het portret in dat kistje.  Stel
de uitspraak op het zilveren kistje is onwaar, dan moet die op het
gouden kistje ook onwaar zijn. Wederom zit het portret in het gouden
kistje. De slimme man wijst dus het gouden kistje aan (als hij haar
tenmiste wil trouwen).


\subsubsection*{Interactieve bewijsverificatie (Mizar)}

\begin{alltt}\footnotesize
theorem
  the_gold_inscription = is_not portrait_in_gold_casket &
  the_silver_inscription =
    exactly_one_holds_of (the_gold_inscription,the_silver_inscription)
implies
  portrait_in_gold_casket is_true
proof
assume that
   A1: the_gold_inscription = is_not portrait_in_gold_casket and
   A2: the_silver_inscription =
     exactly_one_holds_of (the_gold_inscription,the_silver_inscription);
::[in order to prove]
   the_gold_inscription is_false
proof
per cases;
suppose
   A3: the_silver_inscription is_true;
then
   exactly_one_holds_of (the_gold_inscription,the_silver_inscription) is_true
by A2; then
   the_gold_inscription is_true & the_silver_inscription is_false or
   the_gold_inscription is_false & the_silver_inscription is_true
by exactly_one; hence
   the_gold_inscription is_false
by A3; end;
suppose
   A4: the_silver_inscription is_false;
then
   exactly_one_holds_of (the_gold_inscription,the_silver_inscription) is_false
by A2; then
   the_gold_inscription is_true & the_silver_inscription is_true or
   the_gold_inscription is_false & the_silver_inscription is_false
by exactly_one; hence
   the_gold_inscription is_false by A4;
end;
end;
::[in both cases we have the_gold_inscription is_false]
then
   (is_not portrait_in_gold_casket) is_false
by A1; hence
   portrait_in_gold_casket is_true
by is_not_iff_not;
end;
\end{alltt}

Het probleem heeft een logische kronkel. Een van de uitspraken is
verwijst naar zichzelf. In het algemeen leidt dat tot paradoxen
(``Deze uitspraak is onwaar''), maar in dit geval is dat niet zo. In
de technologie van Computer geformaliseerd bewijzen wordt vaak op
gebruik gemaakt van een inzichtelijk betrouwbare vorm van deze
zogenaamde reflectie, verwant aan dit voorbeeld, waarbij wiskundige
uitspraken onderwerp worden van andere uitspraken. Een voorbeeld van
reflectie is het dualiteitsprincipe uit de projectieve meetkunde:
``Een stelling blijft geldig wanneer de begrippen punt en lijn
systematisch verwisseld worden.'' Dit is een stelling over stellingen,
verkregen uit reflectie over de axioma's van de projectieve meetkunde.


\section{\emph{State of the art}}
We noemen een paar systemen die momenteel gebruikt worden. Mizar
(Pools), Coq (Frans), HOL (Engels), Isabelle (Engels/Duits) en PVS
(Amerikaans). Zie respectievelijk de volgende web-sites.
\begin{quote}
\url{www.mizar.org} \\
\url{pauillac.inria.fr/coq/} \\
\url{www.cl.cam.ac.uk/users/jrh/hol-light/} \\
\url{www.cl.cam.ac.uk/Research/HVG/Isabelle/} \\
\url{pvs.csl.sri.com}
\end{quote}
Andere relevante web-site voor Computer Wiskunde (onder meer
over Otter en Automath) zijn de volgende.
\begin{quote}
\url{www-unix.mcs.anl.gov/AR/otter/} \\
\url{automath.webhop.net} \\
\url{www.cs.ru.nl/~freek/aut/} \\
\url{www.cs.ru.nl/~freek/digimath/} \\
\url{www.cs.ru.nl/~freek/qed/qed.html}
\end{quote}
Een greep uit de bibliotheek van geheel geformaliseerde stellingen.
%de
%hoofdstelling van de algebra (ieder polynoom over $\complex$ heeft een
%wortel in $\complex$); de hoofdstelling van de analyse (differenti\"eren
%van de integraal van een continue functie $f$ levert $f$ zelf op);%
De vierkleuren stelling (iedere landkaart in het vlak of de bol kan
met vier kleuren zodanig gekleurd worden dat landen die elkaar aanraken
met meer dan een punt verschillend gekleurd zijn); Bertrand's
postulate (tussen $n$ en $2n$ zit altijd een priemgetal); de
Jordan-curve stelling (een gesloten kromme in het vlak die zichzelf
niet snijdt verdeelt het vlak in twee samenhangende gedeelten); de
priemgetallen stelling (het aantal priemgetallen onder $n$ is in de
orde van $\frac{n}{\log n}$); de onmogelijkheid met een passer en
lineaal een hoek in drie\"en te verdelen of een kubus te verdubbelen.
Toegegeven, dit is nog geen grensverleggende wiskunde, maar het
potentieel om daar te komen is aanwezig. Voor een verdergaande
inleiding in het vak, zie \ncite{barewied05} en \ncite{bare05}.

Ondanks deze initi\"ele successen worden er ook wel bezwaren tegen
Computer Wiskunde ingebracht. Met name dat een bewijs gevrifieerd door
een computer geverifieerd meestal niet begrijpelijk is. Dat kan waar
zijn, maar het bewijs van stellingen met heel lange bewijzen zijn dat
ook niet. De overgang van een overzichtelijke bewijs naar een bewijs
dat niet geheel in het bewustzijn past en door een computer
geverifieerd moet worden, dus van een romantisch naar een \emph{cool}
bewijs, kun je vergelijken met de overgang in de biologie van aandacht
voor bloemen en vlinders naar dat voor genen. De romantische biologie
blijft boeien, maar die van de genen heeft daar direct betrekking op,
meer dan de romantici zouden willen. Een dergelijke verschuiving zal
naar onze mening ook binnen de wiskunde plaats vinden. En net zoals
bij biologie zal menselijk vernuft en vakintu\ui{}tie hard nodig
blijven.

Iedere wiskundige kent het gevoel van tevredenheid wanneer hij of zij
een stelling bewezen heeft. In de computer wiskunde blijft dat het
geval. De emotie wordt nog sterker, want het is duidelijk dat
\emph{alle} details daadwerkelijk ingevuld \emph{zijn}. Bij
romantische bewijzen heeft men de tevredenheid omdat men ervan
overtuigd is dat de details ingevuld \emph{kunnen worden}. Een
niet-wiskundige kan de ervaring van het maken of volgen van een
(gewoon romantisch) bewijs niet goed navoelen. Daarvoor moet men door
de ervaring van het bewijzen heen gegaan zijn. Een vergelijkbaar
effect treedt op bij het maken van een geformaliseerd bewijs: dat kan
alleen naar emotionele waarde geschat worden door het gedaan te
hebben. De intrinsieke waarde van de computer wiskunde ligt in de
volledige duidelijkheid, correctheid en mechanische manipuleerbaarheid
van de resultaten. Bij computeralgebra systemen is dit niveau nog ver
te zoeken.

De verwachting is dat over zeg 10 \`a 50 jaar---een korte periode
vanuit historisch oogpunt bezien---Computer Wiskunde gemeengoed zal
zijn geworden. Menselijke intu\ui{}tie zal samenwerken met de precizie
van een computer. In principe is de huidige stand van de grondslagen
van de wiskunde voldoende om dit nu al te doen. De uitdaging is echter
om de bestaande systemen meer gebruikers-vriendelijk voor wiskundigen
te maken, door voldoende geverifieerde bibliotheken en hulpmiddelen te
ontwikkelen. Het uiteindelijke doel is om mensen te helpen met het
bestuderen, ontwikkelen, communiceren\footnote{Computer wiskunde geeft
vele mogelijkheden voor de electronische communicatie van betrouwbare
resultaten en het voorkomen van `corruptie' van het vak. Deze
corruptie is niet in ethische maar technische zin bedoeld: het
voortbestaan van en vertrouwen op foutieve stellingen. Dat moet worden
tegen gegaan. Zie \ncite{barecohe01}.}, onderwijzen,
verifi\"eren\footnote{Referees die ingezonden artikelen beoordelen
zullen nog steeds nodig zijn; niet voor de correctheid, maar voor het
belang van het werk.} en toepassen van de wiskunde.

\noi ---------------------------------------------------------

Over de auteurs. Henk Barendregt studeerde mathematische logica bij
Dirk van Dalen in Utrecht en promoveerde aldaar op een onderwerp in de
lambda calculus.
Freek Wiedijk studeerde wiskunde en theoretische fysica aan
de Universiteit van Amsterdam en promoveerde aldaar op
een onderwerp in de formele methoden, een deelgebied van de informatica.

  \bibliography{eu}

\end{document}
