Dit artikel is gepubliceerd in NRC Handelsblad, 31 januari 2009
Laat de computer elk wiskundebewijs controleren, vindt een groep wiskundigen en logici. Dan weten we absoluut zeker of een bewijs klopt. Maar het gros van de wiskundigen ziet daar nog niets in.
Als er één wetenschap exact is, dan is het de wiskunde wel. De natuurwetenschappen produceren nooit absolute zekerheden. De wiskunde wel. Toen de stelling van Pythagoras eenmaal was bewezen, gold het bewijs voor eens en 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, zowel de papieren berekeningen, als de computercode en de computerresultaten. Uiteindelijk concludeerden ze dat ze 99% zeker waren dat het bewijs klopt. Ze vermeldden uitdrukkelijk dat ze het niet voor de volle honderd procent hadden kunnen verifiëren. Een unicum in de wiskunde.
Hoe 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 gaat voorkomen 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 naar schatting tussen vijftig en 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,” legt Wiedijk uit, “maken we expliciet en vertalen we voor een computer in een logische taal. Het vertaalde bewijs is dan gemiddeld zo’n viermaal langer dan het gewone wiskundige bewijs. Tussenstapjes die voor iedere wiskundige duidelijk zijn en die hij in het gewone wiskundige bewijs overslaat, moet je uitleggen aan een computer. Naarmate de technologie vordert, zijn er wel minder tussenstapjes nodig. 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 mis gaat, 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 is geëvolueerd tot modernere, krachtigere opvolgers, met als voornaamste vijf: 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.
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 niet een 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, 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 dit 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 ze kunnen checken. De technologie moet alleen verder ontwikkeld worden.”
Punt is echter dat geen enkele wiskundige ook maar de geringste twijfel heeft over de correctheid van de door de computer geverifieerde 81 bewijzen uit de lijst van honderd. Tot nu toe heeft een computer nog geen enkel bewijs gecontroleerd waarover geen honderd procent zekerheid bestaat, en dat kan nog wel even duren ook. Zo werkt Thomas Hales zelf al sinds januari 2003 aan het formaliseren van zijn eigen Keplerbewijs zodanig dat de computer het kan controleren en ook de laatste 1% onzekerheid wegneemt. Hij heeft berekend dat dit project twintig mensjaren gaat kosten. Hales gebruikt het HOL Light-systeem, maar hij richt zich alleen op het automatisch bewijzen van het 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.
Bureaucratische operatie
Hoewel Wiedijk er van overtuigd is dat computerbewijzen de toekomst hebben, geeft hij grif toe dat het gros van de wiskundigen het nog steeds anders ziet: “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 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 zegt dat hij niets principieels heeft tegen bewijsverificatie door een computer, maar wel iets tegen automatische bewijsverificatie als een wereldwijd project voor de hele wiskunde: “Ik ben tegen het idee dat alle wiskundigen in de toekomst hun bewijzen zo moeten opschrijven dat een computer ze kan controleren. Allereerst denk ik niet dat dat zal gebeuren. Hoewel het in principe mogelijk is, is het een veel te arbeidsintensief project, en levert het conceptueel weinig tot niets nieuws. Ten tweede vind ik ook niet dat we die kant uit moeten gaan. Het zou 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 % van de wiskundige bewijzen helemaal geen controleprobleem bestaat: “Daar werkt het traditionele refereeproces prima. Als er al een fout in een bewijs zit, dan vinden mensen deze vroeger of later wel.” Alleen in uitzonderlijke gevallen bestaat er volgens hem een behoefte aan geautomatiseerde bewijsverificatie. Dat is bijvoorbeeld het geval bij het Keplerbewijs en het bewijs van de vierkleurenstelling.
De vierkleurenstelling zegt dat je iedere landkaart met vier kleuren kunt inkleuren zodanig 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 de uitspraak dat het over enkele decennia gebeurt, is ongelofelijk zwak. In de jaren zestig dacht men dat de computer over tien jaar de wereldkampioen schaken zou verslaan. Dat is niet gebeurd. Idem dito in de jaren zeventig. Maar uiteindelijk is het wel gelukt. Hetzelfde kan gebeuren bij het computerbewijs.” Lenstra wil echter 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 de 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 de mechanismen die 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. Daarom houden wiskundigen niet zo van een computerbewijs. Ze kunnen niet zien of het correct is, en waar eventueel een fout zit.”
Opeens herinnert Lenstra zich een persoonlijke ervaring met computerbewijzen, die de scepsis van veel wiskundigen illustreert: “Ik stootte 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 waarover die stelling ging. 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 hij ontdekte een onnozele rekenfout: “Dat betekende dat de stelling toch waar was. De computer had dus uiteindelijk 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. Een computerbewijs voegt daar weinig aan toe.”
Darwiniaanse wiskunde
Wordt het dan wel wat met die computerbewijzen? Wiedijk denkt dat op het moment dat het formaliseren van een bewijs minder werk wordt dan het traditionele controlewerk door mensen, er een omslagpunt optreedt. “Dan zullen referees zeggen: Laat het maar door de computer controleren.” Maar hoe hij de grote meerderheid van sceptische wiskundigen überhaupt zover kan krijgen dat ze energie en geld willen stoppen in computerprogramma’s die bewijzen verifiëren is de grote praktische vraag.
Volgens Lenstra zijn de bewijsprogramma’s die worden geschreven, voor wiskundigen onbegrijpelijk: “Die 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 ook als zijn persoonlijke doel bij de ontwikkeling van de computer als bewijsverificator. Maar ook dat is een project van de lange adem.
Samen met professor Henk Barendregt schreef Wiedijk in een artikel over het computerbewijs dat wiskundigen niet bang hoeven zijn dat de computer hun creativiteit afpakt, en dat het computerbewijs een logische overgang is van romantische wiskunde naar coole wiskunde. Het is vergelijkbaar met de overgang in de biologie van aandacht voor bloemen en vlinders naar die voor genen. Ze schrijven: “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ïtie hard nodig blijven.”
Hoewel het ontrafelen van het wiskundige genoom met de computer in principe mogelijk is, is het maar de vraag of de wiskundige gemeenschap er de menskracht en het geld voor over heeft. Wiedijk heeft uitgerekend dat het formaliseren van de belangrijkste bewijzen uit de wiskunde met het budget van een populaire Hollywoodfilm te doen is. “Maar ja,” voegt hij toe, “die film brengt daarna geld op, en onze bewijssystemen niet.”
Misschien gaat de wiskunde door de toenemende complexiteit van bewijzen wel meer op de exacte natuurwetenschappen lijken, waar absolute zekerheid ook niet bestaat. Het controleren van bewijzen wordt dan nog meer een sociaal en Darwiniaans proces dan het nu is: een survival of the fittest van wiskundige bewijzen. Toch blijft zelfs dan de wiskundige exactheid ongeëvenaard vergeleken met die van alle andere wetenschappen. “Maar,” besluit Wiedijk, “als ik gelijk krijg, en computerbewijzen gaan echt een grote vlucht nemen, dan wordt de wiskunde eindelijk echt ‘wis’.”
[kader:]
Kan de computer ook zelf nieuwe wiskunde ontdekken?
Wanneer de computer een bewijs controleert, controleert hij stapje voor stapje of de mens geen fout heeft gemaakt. Nog steeds is het de wiskundige die het bewijs heeft bedacht. Maar zou een computer ook zelf nieuwe wiskunde kunnen ontdekken? “In specifieke takken, zoals de computeralgebra, denk ik dat de computer zelf nieuwe wiskunde kan ontdekken”, zegt professor Ulrich Kohlenbach van de Technische Universiteit Darmstadt. “Dat is op bescheiden schaal ook al gebeurd in de computeralgebra. Maar ik geloof niet dat we de computer ooit voor de hele wiskunde beter wordt dan de mens.”
Ook Freek Wiedijk van de Radboud Universiteit Nijmegen denkt dat de computer nauwelijks zal bijdragen tot het ontdekken van conceptuele nieuwe wiskunde: “Automatische stellingenbewijzers zijn vreselijk interessant, maar kunnen vaak zelfs niet eens ‘makkelijke stapjes’ in een bewijs zelf doen. Laat staan dat ze met intelligente suggesties kunnen komen. De computer moet je volgens mij zien als een relatief domme maar zeer precieze en daarom zeer waardevolle boekhouder, niet als een geautomatiseerde versie van een menselijke assistent. Net zoals je een tekstverwerker ook niet moet zien als een assistent die je helpt een artikel te schrijven. Sommigen beweren dat computers de wiskundigen al hebben ingehaald. Dat geldt echter alleen voor specifieke puzzelbewijzen: problemen met veel mogelijkheden. Maar dat is niet conceptueel. De computer is natuurlijk wel enorm nuttig om allerlei voorbeelden door te rekenen. Zo verzamelt hij als het ware experimenteel materiaal waarop de mens zijn intuïtie kan loslaten.”
Professor Hendrik Lenstra van de Universiteit Leiden is iets optimistischer: “Ik zie niet waarom het principieel onmogelijk is voor de computer om nieuwe wiskunde te ontdekken, maar daar staan we wel nog ver van af. Wiskundigen zijn sterk in het conceptualiseren van een bewijs. Om dat te automatiseren, is een enorme dobber.”
Internet
Speciale editie van de Notices van de American Mathematical Society over computerbewijzen (december 2008):
www.ams.org/notices/200811/
De top 100 van wiskundige stellingen, en welke daarvan met welk computersysteem zijn geverifieerd:
www.cs.ru.nl/~freek/100/index.html
Bewijzen: romantisch of cool?:
ftp://ftp.cs.kun.nl/pub/CompMath.Found/euclides.pdf
Voor wie wil zien hoe een computerbewijs van een eenvoudige stelling (‘Er is geen grootste priemgetal’) eruit ziet, vergeleken met het gewone wiskundige bewijs: www.cs.ru.nl/~freek/pubs/pythagoras.pdf
Het Flyspeck-project van Thomas Hales om zijn eigen bewijs van het Keplerprobleem door een computer te laten verifiëren: http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet
Het QED-manifest uit 1994 beschrijft een toekomst waarin alle wiskundige bewijzen in de computer zijn gecodeerd:
www.cs.ru.nl/~freek/qed/qed.html
