Computerbewijzen in de wiskundige praktijk

Gaan computers wiskundigen vervangen?



'Een wiskundige is een machine om koffie in stellingen om te zetten,' zei de Hongaarse wiskundige Paul Erdös ooit. Zo vanzelfsprekend is het bewijzen van wiskundige vermoedens echter niet. Naast koffie vergt het ook veel bloed, zweet en tranen en soms honderden jaren werk voordat wiskundigen een moeilijk vermoeden kunnen bewijzen. In de twintigste eeuw hebben een aantal computerprogramma's zelfs stellingen bewezen die te moeilijk zijn voor onze beste wiskundigen. Worden wiskundige stellingen in de toekomst het alleenrecht van échte machines?



In 1997 versloeg Deep Blue, een supercomputer van IBM, toenmalig wereldkampioen Gary Kasparov in een schaaktoernooi. Eind 2006 werd Kasparovs opvolger Vladimir Kramnik in een toernooi verslagen door het schaakprogramma Deep Fritz 10. Ditmaal was er geen supercomputer meer nodig, maar een flink uit de kluiten gewassen bureaucomputer. In juli 2007 wonnen twee professionele pokerspelers maar nipt van een pokerprogramma. Het is nog maar een kwestie van tijd totdat de wereldkampioen poker verslagen wordt door een computer.



De nederlaag van Kasparov tegen Deep Blue bracht heel wat emoties los: mensen vonden dat computers schaak dood maakten. Anderen beweerden dat Deep Blue niet 'echt' schaak speelt, omdat de computer immers niets van schaak begrijpt: het is maar een massa rekenwerk. Ook de wiskundige bewijzen die door computerprogramma's geleverd werden, kregen te maken met zo'n negatieve reacties. Filosofen zeurden dat computerbewijzen geen échte wiskundige kennis geven en wiskundigen vonden dat deze bewijzen hen geen inzicht gaven in waarom de stelling juist geldt. Vooral dat laatste is problematisch: de computer zegt je wel dat de stelling waar is, maar je hebt er geen flauw idee van waarom, omdat het bewijs van de computer veel te lang en te ingewikkeld is.



Het eerste grote computerbewijs werd in 1976 afgewerkt door de Amerikaanse wiskundigen Kenneth Appel en Wolfgang Haken. Hun programma bewees de vierkleurenstelling. Deze stelling zegt dat het voor een willekeurige landkaart mogelijk is om de landen met hoogstens vier kleuren zó in te kleuren dat geen twee aangrenzende landen dezelfde kleur hebben. Met aangrenzend bedoelen we dat de landen een grens delen, dus landen die slechts in een punt aan elkaar liggen (zoals twee overliggende spieën van een gesneden taart) zijn niet aangrenzend. Met een land bedoelen we bovendien een samenhangend deel van de kaart, dus bijvoorbeeld niet de Verenigde Staten met Alaska erbij. Een student formuleerde in 1852 het vermoeden dat elke kaart op deze manier met vier kleuren in te kleuren is, waarna heel wat wiskundigen zich over het probleem bogen.



Het uiteindelijke bewijs van Appel en Haken bestond uit twee delen: het eerste deel beschreef de globale bewijsstrategie en een groot aantal regels om een verzameling van mogelijke delen van een kaart te construeren. Het tweede deel somde een zogenaamde 'onvermijdelijke verzameling' van delen van een kaart op: elke mogelijke kaart bevat minstens één deelkaart uit deze verzameling. De wiskundigen hadden ook een computerprogramma geschreven dat van elk van deze deelkaarten probeerde te bewijzen dat het niet kan voorkomen in een kaart waarvoor vijf kleuren nodig zijn. De rest van het bewijs bestond uit massa's berekeningen door de computer. Hieruit bleek dat inderdaad geen enkel van deze deelkaarten kan voorkomen in een kaart waarvoor vijf kleuren nodig zijn. En aangezien elke kaart minstens één van deze deelkaarten bevat, hadden ze zo bewezen dat elke kaart maximum vier kleuren nodig heeft om correct ingekleurd te worden.



De reacties op dit bewijs waren hevig. Zo kloegen veel wiskundigen dat de berekeningen van de computer veel te uitgebreid waren om te kunnen nakijken, zoals ze bij een klassiek bewijs gewoon waren. Daarom konden ze niet zeker zijn of het bewijs wel correct is. Anderen ontkenden zelfs dat het een bewijs was. Zo vergeleek de wiskundige Bonsall het accepteren van een computerbewijs met het accepteren van het woord van een andere wiskundige die zegt dat hij de stelling heeft bewezen, maar het bewijs niet geeft. Wiskundigen begrijpen het bewijs volgens hem niet, en hij noemt computerbewijzen dan ook 'quasi-bewijzen'. De wiskundige Paul Halmos ging zelfs verder: 'Het huidige bewijs [van de vierkleurenstelling] vertrouwt eigenlijk op een orakel, en ik zeg "weg met orakels!" Dit is geen wiskunde.'



Haken werd na zijn bewijs soms zelfs vijandig benaderd. Eén wiskundige probeerde te vermijden dat Haken contact kreeg met de studenten in zijn departement. Omdat het bewijs van de vierkleurenstelling was geleverd, zouden andere wiskundigen volgens hem niet meer proberen om een alternatief bewijs te vinden. Alle eer gaat immers naar het eerste bewijs. Maar omdat Haken het probleem op een 'ongepaste' manier had opgelost, aldus die collega, zou een beter bewijs er nooit komen. Haken vertelt hierover: 'We hadden iets heel ergs gedaan en zoiets mocht niet meer gebeuren, en daarom moest hij de onschuldige zielen van zijn studenten tegen ons beschermen.



'Gelukkig waren er ook nog nuchtere geesten, zoals de wiskundige Edwart Swart, die ook had geprobeerd om de vierkleurenstelling te bewijzen. Hij zag het belang van het computerbewijs in en begreep al die hysterie niet: 'Waarom zouden we wel bewijzen met potlood en papier aanvaarden, maar geen bewijzen met behulp van een computer?' Een bewijs dat gebruik maakt van computerberekeningen zag hij gewoon als een uitbreiding van hulpmiddelen als pen en papier.



Anno 2007 zijn er niet veel wiskundigen meer die echt twijfelen aan de correctheid van computerbewijzen. Dit komt enerzijds omdat wiskundigen meer en meer vertrouwd zijn met computers. Programma's als Mathematica en Maple om wiskundige berekeningen uit te voeren staan op de pc van veel wiskundigen. Anderzijds bestaan er ondertussen ook computerprogramma's die de correctheid van bewijzen in digitale vorm kunnen nagaan. Als het programma zo'n computerbewijs met succes nagekeken heeft, kunnen we er zeker van zijn dat het bewijs correct is, tenzij het programma zelf niet correct is. Maar dit programma is veel kleiner dan de meestal grote computerbewijzen, dus wiskundigen kunnen de correctheid van het programma nagaan.



Een probleem dat echter blijft, is dat computerbewijzen vaak niet inzichtelijk zijn. Het zijn vaak lange berekeningen die niemand in zijn geheel kan nakijken. Als je delen ervan nakijkt, zie je ook niet echt de ideeën die achter het bewijs zitten. Je verliest jezelf al vlug in het nakijken van een hoop details. Dat is dan ook één van de redenen waarom veel wiskundigen wel computerprogramma's zoals Mathematica gebruiken om berekeningen uit te voeren, maar slechts weinig wiskundigen computerprogramma's gebruiken om delen van een bewijs te construeren.



Uit deze studie blijkt dat het idee van wiskundigen als machines om koffie in stellingen om te zetten niet zo vruchtbaar is. Voor wiskundigen telt immers meer dan enkel het resultaat. Wat er in het hoofd van een wiskundige gebeurt is even belangrijk als de koffie die erin gaat en de stelling die eruit gaat. Hetzelfde geldt voor computers: niet enkel de bits die je erin giet en het antwoord 'de stelling klopt' zijn belangrijk, ook de manier waarop de computer de stelling bewezen heeft. Zolang de computer dit niet zoals een echte wiskundige doet, kan hij nooit de wiskundige vervangen.Koen Vervloesem