QED zegt de computer

Laat de computer elk wiskundebewijs controleren, vindt een groep wiskundigen en logici. Dan weten we zeker of een bewijs klopt. Maar de meeste wiskundigen zien daar niets in. Bennie Mols

Als er één wetenschap exact is, dan is het de wiskunde. Andere wetenschappen produceren nooit absolute zekerheden. De wiskunde wel. Toen de stelling van Pythagoras eenmaal was bewezen, gold het bewijs voor eens en voor altijd.

Toch lijkt er een kentering te ontstaan in die absolute zekerheid. Wiskundige bewijzen zijn in de loop van de tijd steeds complexer en langer geworden. Zo complex, dat collega-wiskundigen die een bewijs controleren, het soms ook niet meer zeker weten. Honderden pagina’s bewijs zijn geen uitzondering meer.

In 1998 gaf de Amerikaanse wiskundige Thomas Hales een bewijs voor een bijna vier eeuwen oud wiskundeprobleem: het Keplervermoeden (1611). De vraag is hoe je sinaasappels, tennisballen of knikkers zo efficiënt mogelijk op elkaar stapelt. Elke groenteboer heeft in de praktijk het antwoord al gevonden, maar hoe bewijs je dat die stapeling inderdaad de ruimte het meest efficiënt vult? Hales puzzelde het uit en had daarvoor onder andere veertigduizend regels computercode nodig.

Nu is een bewijs pas een geldig bewijs als andere wiskundigen het er gezamenlijk over eens zijn dat het klopt. Vier jaar lang bogen twaalf experts zich over het bewijs van Hales. Ze ploegden zich door de papieren berekeningen, en ook door de computercode en de computerresultaten. Uiteindelijk concludeerden ze dat ze 99 procent zeker waren dat het bewijs klopt. Ze vermeldden uitdrukkelijk dat ze het niet voor de volle 100 procent hadden kunnen verifiëren. Een unicum in de wiskunde en heel frustrerend. Want wat heb je aan een bewijs als er een kleine kans is dat het niet klopt? Een beetje fout bewijs bestaat net zo min als een beetje zwanger zijn.

De Hongaarse wiskundige Gábor Fejes Tóth, projectleider bij de controle van het bewijs van Hales, meent dat het steeds vaker zal gebeuren dat wiskundigen niet meer absoluut overtuigd kunnen zijn van de geldigheid van een bewijs, en dat ze daar maar aan moeten wennen.

PERFECTE BOEKHOUDER

Maar er is een oplossing, zo denkt een groep van zo’n vijftig tot honderd wiskundigen en logici. Een kleine minderheid in de wereld van wiskundigen, maar toch. Ze zijn sterk van hun missie overtuigd. Ze willen de computer gebruiken om bewijzen te controleren en zo de absolute zekerheid terug winnen.

Een van die wiskundigen is dr. Freek Wiedijk van het Institute for Computing and Information Sciences van de Radboud Universiteit Nijmegen. Samen met een tiental Nijmeegse collega’s onder leiding van professor Henk Barendregt gebruikt hij een computersysteem om wiskundige bewijzen te controleren.

“Elke stap die een wiskundige in zijn hoofd maakt”, zegt Wiedijk, “maken we expliciet en vertalen we voor een computer in een logische taal. Het vertaalde bewijs is gemiddeld circa viermaal langer dan het gewone wiskundige bewijs, want tussenstapjes die voor iedere wiskundige duidelijk zijn en die hij in het gewone wiskundige bewijs overslaat, moet je uitleggen aan een computer. De computer loopt vervolgens alle stappen na en controleert of ze voldoen aan de logische regels van het systeem. Klopt er iets niet in het bewijs, dan geeft de computer precies aan wat er misgaat, en waar. Hij doet hierbij niets wat een mens niet kan, maar hij maakt geen fout in de boekhouding. Veel wiskundigen kunnen zich die perfectie niet voorstellen, maar het is een feit.”

Nieuw is het idee niet. De Nederlander Dick de Bruijn was een van de pioniers in de controle van wiskundige bewijzen door een computer. Sinds 1968 werkte hij aan het project Automath, dat hetzelfde doel had als Wiedijk, Barendregt en anderen nu hebben. Automath heeft inmiddels een aantal krachtige opvolgers gekregen. De voornaamste vijf zijn: Coq (Frans), Isabelle (Engels/Duits), HOL Light (Engels), Mizar (Pools) en ProofPower (Engels). Elk systeem bouwt in zijn eigen logische taal stukje bij beetje een bibliotheek op van bewezen stellingen. Hoe groter de bibliotheek, hoe meer nieuwe wiskundige bewijzen het systeem aan kan.

Maar kan het computerprogramma dat een bewijs controleert niet een bug bevatten, zoals vaak bij ingewikkelde programma’s? Die kans wordt op twee manieren geminimaliseerd, vertelt Wiedijk. Allereerst hoef je bij het computerprogramma maar eenmaal na te gaan of het correct is. Daarna kun je het programma voor allerlei soorten bewijzen gebruiken. Ten tweede worden de programma’s zo geschreven dat de essentie in een klein deel van het totale programma zit. Als die kern bugvrij is, dan is de bewijsverificatie ook bugvrij. Wiedijk: “De kans dat er een bug optreedt die effect heeft op het bewijs, is op deze manier nihil. Het is ons nog nooit gebeurd. We zijn nu zelfs met de computer aan het ‘bewijzen’ dat het essentiële stukje van het programma bugvrij is. Als dat klaar is, hoeven we ons helemaal geen zorgen meer te maken over bugs in ons programma.”

Automatische bewijsverificatie is zeker niet alleen een universitair speeltje. Zowel softwarefabrikant Microsoft als chipfabrikant Intel hebben wiskundigen in dienst die bewijsverificatoren ontwikkelen. Intel gebruikt de bewijsverificator bijvoorbeeld om te bewijzen dat er geen bug in een nieuw type chip zit. In 1994 kostte een bug in de Pentiumchip het bedrijf veel geld en dat mag geen tweede keer gebeuren.

Wat heeft het ontwikkelen van automatische bewijsverificatoren tot nu toe opgeleverd? Wiedijk: “Aan het Poolse Mizar-systeem wordt het langst gewerkt, al sinds 1974. Het bevat inmiddels zo’n vijftigduizend stellingen die zijn geformaliseerd en die de computer heeft goedgekeurd. En als je de lijst van honderd mooiste wiskundige bewijzen neemt (zie kader) dan zijn er daar inmiddels 81 van door een computer geverifieerd. Nu zijn computerbewijzen nog een soort kunst omwille van de kunst. Maar ik ben er van overtuigd dat het de toekomst van de wiskunde wordt. Over enkele decennia zullen wiskundigen blij zijn met de computer als bewijsverificator. Er is namelijk geen fundamenteel obstakel om bewijzen zo te formaliseren dat computers die kunnen checken. De technologie moet alleen verder ontwikkeld worden.”

ZEKERHEID

Punt is echter dat geen enkele wiskundige vooraf ook maar de geringste twijfel had over de correctheid van de door de computer geverifieerde 81 bewijzen uit de lijst van honderd. En tot nu toe heeft een computer nog geen bewijzen gecontroleerd waarover géén 100 procent zekerheid bestaat, en dat kan nog wel even duren ook. Zo werkt Thomas Hales zelf al sinds januari 2003 aan het zodanig formaliseren van zijn eigen Keplerbewijs dat de computer het kan controleren en ook de laatste 1 procent onzekerheid wegneemt. Hij heeft berekend dat dit project twintig mensjaren zal kosten.

Hales gebruikt het HOL Light-systeem, maar hij richt zich alleen op het automatisch bewijzen van zijn Keplerprobleem.

Veel wiskundigen vinden dat Hales zijn tijd beter kan besteden aan het bedenken van nieuwe wiskunde dan aan het formaliseren van zijn eigen bewijs. Maar Hales beschouwt het formaliseren van de belangrijkste bewijzen uit de wiskunde als ‘het ontrafelen van het wiskundige genoom’. Het is een oude droom van wiskundigen en logici: de hele wiskunde van onderaf helemaal uit de logica opbouwen, met zo min mogelijk aannames. Maar die droom is tot nu toe nooit uitgekomen.

Hoewel Wiedijk ervan overtuigd is dat computerbewijzen de toekomst hebben, geeft hij grif toe dat de meeste wiskundigen het nog steeds anders zien: “Wiskundigen zijn er niet in geïnteresseerd en geloven er nog niet in. Helaas.”

Eén van de wiskundigen die behoort tot de grote groep van critici van zo’n wiskundig-genoomproject is de Duitse wiskundige en logicus professor Ulrich Kohlenbach van de Technische Universiteit van Darmstadt: “In zekere zin klopt het wat Hales zegt over het ontrafelen van het wiskundige genoom. Maar het is net als in de biologie. Kennis van het genoom betekent niet dat je de biologie van de mens begrijpt. Evenzo is wiskunde meer dan een verzameling van geformaliseerde bewijzen die op een of andere server staan. Wiskunde is een uitwisseling van ideeën tussen mensen. Mensen moeten die ideeën begrijpen, anders bestaan ze niet.”

Kohlenbach heeft niets principieels tegen bewijsverificatie door een computer, zegt hij, maar hij heeft er wel iets tegen als dat een wereldwijd project voor de hele wiskunde wordt: “Ik ben tegen het idee dat alle wiskundigen in de toekomst hun bewijzen zo moeten opschrijven dat een computer ze kan controleren. Veel te arbeidsintensief en het levert conceptueel weinig tot niets nieuws. Ten tweede zou het de aandacht verschuiven van het bewijzen van nieuwe resultaten naar een bureaucratische operatie van het routinematig checken van wiskundige kennis. Dan moeten we wiskunde voor machines gaan schrijven in plaats van wiskunde voor mensen.”

Kohlenbach vindt dat er voor 99,99 procent van de wiskundige bewijzen helemaal geen controleprobleem bestaat: “Als er al een fout in een bewijs zit, dan vinden mensen dit vroeger of later wel.” Alleen in uitzonderlijke gevallen bestaat er volgens hem behoefte aan geautomatiseerde bewijsverificatie. Bijvoorbeeld bij het Keplerbewijs en het bewijs van de vierkleurenstelling.

De vierkleurenstelling zegt dat je iedere landkaart zodanig met vier kleuren kunt inkleuren dat landen die elkaar in meer dan een punt aanraken verschillend gekleurd zijn. Kenneth Appel en Wolfgang Haken gaven in 1976 een bewijs dat zevenhonderd pagina’s papieren redenering combineerde met 1200 uur computerrekentijd, een gruwel voor veel wiskundigen in die tijd. De grap gaat dat wiskundigen boven de veertig niet overtuigd konden worden dat het computerbewijs klopt, en dat de wiskundigen onder de veertig niet overtuigd konden worden dat het zevenhonderd pagina lange papieren bewijs klopt.

'PATROONHERKENNING

De Leidse wiskundige professor Hendrik Lenstra staat neutraal in de discussie over het computerbewijs. “Ik zie geen reden waarom de computer niet op grote schaal gebruikt zal worden om bewijzen te verifiëren.” Maar Lenstra wil benadrukken dat wiskunde veel meer is dan bewijzen. “Weten of iets waar is, is niet de eerste bezigheid van wiskundigen. We willen weten waarom iets waar is. Ons vak is niet het controleren van bewijzen, maar het produceren van bewijzen.”

Het produceren van een bewijs is vooralsnog een menselijke bezigheid. Lenstra: “Als je een bewijs bedenkt, dan doe je voor een groot deel aan patroonherkenning. Je legt een associatie met iets wat je eerder bent tegengekomen, soms zelfs in een andere tak van de wiskunde. Je bent niet in eerste instantie geïnteresseerd in de inhoud van bepaalde stellingen, maar in het mechanisme dat achter hun waarheid steekt. Als je dat begrijpt, dan kun je het ook in een andere situatie toepassen. Dan heb je weinig aan de mededeling dat die stelling correct is.”

Lenstra herinnert zich een persoonlijke ervaring met computerbewijzen. “Ik stuitte op een stelling die niet uit mijn eigen vakgebied kwam en ik wilde weten of de stelling waar of onwaar was. Ik zag dat een computer het antwoord moest kunnen berekenen. Ik heb het toen voorgelegd aan iemand uit de computeralgebra. Hij programmeerde het probleem en na een dag rekenen gaf de computer het antwoord dat de stelling ‘waar’ was. Een tijd later kwam ik een expert tegen op het terrein van die stelling. Ik legde hem mijn probleem voor en hij zei: ‘dat reken ik zo voor je uit’. Hij pakte een servetje, mompelde wat, krabbelde wat op het servetje en na een tijdje zei hij: ‘de stelling is onwaar’. Toen dacht ik: fijn, ik weet nu nog niet wie gelijk heeft, maar dat servetje kan ik goed gebruiken. Die expert kent de theorie, hij heeft zijn redenering opgeschreven, dus ik kan het narekenen.”

Lenstra nam het servetje mee, ging bestuderen welke redeneringen de expert had gebruikt en ontdekte op het servetje een onnozele rekenfout: “Dat betekende dat de stelling toch waar was. De computer had dus gelijk. Maar belangrijker was dat ik nu begreep waarom, omdat ik de achterliggende theorie begreep. Toen ik de theorie voorlegde aan degene die mijn probleem had geprogrammeerd, kon hij het probleem veel handiger programmeren. In plaats van na een dag rekenen, kregen we na een halve minuut al het antwoord. Echte stappen voorwaarts maak je pas als je het in je hoofd begrijpt.”

Wordt het dan wel wat met die computerbewijzen? Wiedijk denkt dat er een omslagpunt optreedt op het moment dat het formaliseren van een bewijs minder tijd vergt dan het traditionele controlewerk door mensen. “Dan zullen referees zeggen: Laat het maar door de computer controleren.” Maar de grote praktisch vraag is hoe hij de meerderheid van sceptische wiskundigen überhaupt zover kan krijgen dat ze energie en geld willen stoppen in computerprogramma’s die bewijzen verifiëren.

Volgens Lenstra zijn de huidige bewijsprogramma’s voor wiskundigen onbegrijpelijk: “De programma’s zouden veel dichter bij de gebruikelijke wiskundige taal moeten aansluiten, liefst zelfs bij de natuurlijke taal.”

Wiedijk is het daar helemaal mee eens en ziet dat als zijn persoonlijke doel bij de ontwikkeling van de computer als bewijsverificator. Maar ook dat is een project van lange adem. Wiedijk heeft uitgerekend dat het formaliseren van de belangrijkste bewijzen uit de wiskunde met het budget van een populaire Hollywoodfilm te doen is. “Alleen”, zegt hij, “die film brengt daarna geld op en onze bewijssystemen niet.”