Je leest:

Formele bewijzen: het DNA van de wiskunde

Formele bewijzen: het DNA van de wiskunde

Auteurs: en | 14 november 2008

Het decembernummer van de Notices of the American Mathematical Society heeft als thema ‘formal proof’, met artikelen over de recentste ontwikkelingen van door computers gegenereerde en door computers geverifieerde bewijzen.

In tegenstelling tot wat je misschien zou verwachten, gebruiken wiskundigen computers nauwelijks om wiskunde mee te doen. Ze gebruiken ze als tekstverwerker (om hun artikelen en boeken mee te schrijven) en ze gebruiken ze voor experimenten (om te bekijken hoe speciale gevallen van hun stellingen zich gedragen). Traditionele wiskundigen gebruiken de computer echter niet voor de bewijzen van hun stellingen: wiskundige bewijzen zitten in mensenhoofden en worden opgeschreven in een mengeling van (vaak) Engels en wiskundige symbolen. Ze verwijzen daarbij naar vroegere resultaten, laten makkelijke kwesties open die als ‘triviaal’ worden beschouwd en doen vaak een beroep op intuïtie. De correctheid van zo’n bewijs wordt bepaald door referees en andere wiskundigen die de argumenten nalezen of erover discussiëren. Dit is in essentie een sociaal proces. Meestal werkt dit, maar er zijn verschillende voorbeelden van foute resultaten die in eerste instantie als correct werden beschouwd: de referees hadden dan een fout in het vermeende bewijs over het hoofd gezien.

Als een bewijs erg ingewikkeld en lang is (sommige wiskundige bewijzen tellen tientallen of honderden pagina’s), is de kans op een lek best groot. Een beroemd voorbeeld is het bewijs van de Laatste Stelling van Fermat van Andrew Wiles: hij kwam in 1993 – na zeven jaar in stilte te hebben gewerkt – met zijn bewijs naar buiten. Een van de referees ontdekte een fout waardoor het hele verhaal op losse schroeven kwam te staan. Gelukkig wist Wiles zijn fout zelf te repareren. In 1994 werd zijn bewijs geaccepteerd door de wiskundige gemeenschap en in 1995 verscheen het ruim honderd pagina’s tellende bewijs in het prestigieuze tijdschrift Annals of Mathematics.

Het vierkleurenprobleem

Elke platte landkaart die je maar kunt tekenen is met maximaal vier verschillende kleuren in te kleuren, zonder dat aangrenzende landen gelijke kleur hebben. Zo luidt het ‘vierkleurenprobleem’. Dit probleem werd in 1852 opgeworpen door Francis Guthrie, waarna wiskundigen probeerden te bewijzen dat vier kleuren inderdaad altijd genoeg is. In 1976 werd door Kenneth Appel en Wolfgang Haken een bewijs geleverd dat gebruik maakt van de computer, waarin zo’n 1500 ‘configuraties’ onderzocht werden, ieder leidend tot duizenden gevallen. Sceptici keurden dit computerbewijs af, omdat ze niet vertrouwden op de berekeningen die de computer maakte.Sinds 1994 is er een tweede bewijs (van Neil Robertson en anderen), dat eveneens gebruik maakt van de computer. In dit bewijs is het aantal configuraties teruggebracht tot 633 en werd de complexiteit van de controle per configuratie teruggebracht. Maar ook toen ontstond er discussie over de betrouwbaarheid van de nog steeds omvangrijke computerberekeningen. Maar in 2004 presenteerde de Fransman Georges Gonthier een versie van Robertsons bewijs, die zo nauwkeurig uitgeschreven is dat de juistheid van elke stap gecontroleerd kon worden. Die controle werd uitgevoerd door de ‘bewijs-assistent’ Coq: een programma van Franse origine, dat de juistheid van wiskundige bewijzen verifieert.

Bewijzen nalopen met de computer

De twintigste eeuw kende een explosie van wiskunde en ook een explosie van complexe bewijzen die honderden pagina’s innemen. Sommige van deze bewijzen zijn bovendien gebaseerd op ellenlange berekeningen op een computer, samen met ingewikkelde computercode (zie de kaders ‘Het vierkleurenprobleem’ hierboven en ‘Het vermoeden van Kepler’ hieronder). Dit soort bewijzen is een grote uitdaging voor wiskundigen, want de correctheid hiervan is in de praktijk niet na te gaan.

Om deze uitdagingen aan te kunnen gaan, hebben een aantal informatici en wiskundigen computertools ontwikkeld die volledig formele bewijzen helpen opstellen, waarvan elke logische stap automatisch kan worden gecontroleerd om de correctheid voor eens en voor altijd na te gaan. Sommige van deze computerprogramma’s kunnen ook zelf proberen om een bewijs van een opgegeven stelling te maken en gaan dan zelf op zoek naar de nodige tussenstappen. Voor eenvoudige stellingen lukt dit al. Als deze programma’s in de toekomst verbeteren, zouden we van alle belangrijke stellingen in de wiskunde een formeel bewijs kunnen leveren, dat volgens wiskundige Thomas Hales dan zoiets zou vormen als ‘the sequencing of the mathematical genome’.

Thomas Hales. Foto Rebecca Droke, Post-Gazette

Het vermoeden van Kepler

Hoe stapel je sinaasappels zo compact mogelijk op? Johannes Kepler gaf in 1611 het antwoord: bouw met je sinaasappels een piramide. Hij gaf echter geen bewijs voor zijn stelling dat dit inderdaad de efficiëntste manier van stapelen is. In 1998 beweerde de Amerikaan Thomas Hales het vermoeden van Johannes Kepler te hebben bewezen. Hales’ bewijs berust voor een groot deel op rekenwerk met een computer. Zijn bewijs werd door de Annals of Mathematics met gemengde gevoelens ontvangen. Het duurde zo’n vijf jaar voordat het team van twaalf referees het bewijs had gecontroleerd. Het hoofd van het team referees, Gábor Fejes Tóth, zei dat ze 99% zeker waren van de correctheid van het bewijs, maar dat ze de correctheid van alle computerberekeningen niet konden garanderen omdat ze niet elke lijn computercode konden nakijken. De editors van Annals besloten om Hales’ bewijs in tweeën te splitsen: ze publiceerden enkel het theoretische gedeelte van het bewijs, dat op de traditionele manier door referees was nagekeken. Dit deel beschouwden ze als een correct en zelfs hoogstaand bewijs. Voor de publicatie van het computergedeelte moest Hales zijn toevlucht zoeken tot het gespecialiseerde tijdschrift Discrete and Computational Geometry. Mede door deze ervaring is Hales begonnen met het Flyspeck-project, een volledig formeel en door computers geverifieerd bewijs van het Keplervermoeden. Hij vermoedt dat dit zo’n twintig jaren zal vereisen. Afbeelding: Bob Kalmbach

Zie ook:

Nieuwste ontwikkelingen

Het decembernummer van de Notices of the American Mathematical Society heeft als thema ‘formal proof’, met artikelen over door computers gegenereerde en door computers geverifieerde bewijzen. De volgende vier artikelen van experts geven een overzicht van de nieuwste ontwikkeling in het domein van formele bewijzen en de computertools daarvoor. Een van de artikelen is van de Nederlander Freek Wiedijk van de Radboud Universiteit in Nijmegen. Zijn vakgroep verricht baanbrekend werk op het gebied van computerbewijzen.

Dit artikel is een publicatie van NEMO Kennislink.
© NEMO Kennislink, sommige rechten voorbehouden
Dit artikel publiceerde NEMO Kennislink op 14 november 2008

Discussieer mee

0

Vragen, opmerkingen of bijdragen over dit artikel of het onderwerp? Neem deel aan de discussie.

NEMO Kennislink nieuwsbrief
Ontvang elke week onze nieuwsbrief met het laatste nieuws uit de wetenschap.