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.

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’.

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.