Onze andere sites
Spinoza.tv

Henk Barendregt - Wiskundig inzicht

Laat de computer wiskundige stellingen bewijzen

De wiskunde wordt terecht beschouwd als een van de meest exacte wetenschappen. Mathematische correctheid berust op strenge definities, bewijzen en berekeningen. Daardoor heeft het vak een precisie, kracht en zekerheid ‘welke in het dagelijkse leven hun weerga niet kennen’ (R. Musil). Toch is beoefening van wiskunde fenomenologisch: bewijzen van stellingen zijn gebaseerd op menselijk inzicht en informele redeneerstappen die voor mensen evident zijn.

In de grondslagen van de wiskunde wordt bestudeerd wat de achtergronden zijn van genoemde inzichten. Een verbazend klein aantal regels blijkt voldoende voor het machtige bouwwerk van de wiskunde. Men is er zelfs in geslaagd om stukken door mensen bedachte wiskunde zó volledig te ‘formaliseren’, dat computers (de zogeheten wiskundige assistenten) deze stap voor stap zelfstandig kunnen verifiëren.
Menselijke oordeel blijft echter nodig, om te bepalen of een wiskundige theorie interessant is. Bijvoorbeeld: is deze van toepassing binnen andere takken van wetenschap of zelfs andere takken van de wiskunde.
Met de volgende stelling zijn de meeste wiskundigen het niet eens. “Het is de moeite waard om grote delen van de wiskunde te formaliseren.” Er zijn verschillende redenen – niet allemaal gebaseerd op kennis van zaken – waarom men dit niet wil.

1. Moeilijk: Het is veel werk om gewone wiskunde te formaliseren: dit kost doorgaans ongeveer vier keer zoveel pagina’s en tien keer zoveel tijd.
2. Geen voordelen. We zijn al zeker van onze zaak. Er is geen grotere graad van precisie en kracht. Het formaliseren heeft dus geen nut.
3. Wel nadelen. Door het formaliseren haalt men de wiskunde-ervaring weg uit het denken van de wiskundige. Men kan formele bewijzen niet intuïtief overzien.
4. Mogelijke onbetrouwbaarheid. Wanneer wiskunde van computers afhankelijk wordt, dan wordt deze dubieus. Want al heeft men de correctheid van het verifiërende programma ingezien, dan nog is men afhankelijk van de correctheid van de hardware, het operating systeem, de compiler en toevallige kosmische stralen (die bijvoorbeeld de inhoud van één geheugenbit kunnen veranderen), die het functioneren van een computer en zijn geheugen kunnen frustreren.

Mijn reactie op deze tegenwerpingen:
Ad 1. Formaliseren is inderdaad moeilijk, maar wel mogelijk. De vierkleurenstelling, inclusief een zeer lange berekening en bewijs van relevantie van deze berekening, is volledig geformaliseerd door G. Gonthier, en geverifieerd door de wiskundige assistent Coq. Door in te zien hoe de menselijke, intuïtieve redeneerstappen automatisch onderbouwd worden en door bijbehorende gecertificeerde software te schrijven, zal de onbetrouwbaarheid waarschijnlijk naar beneden bijgesteld kunnen worden, hetgeen bijvoorbeeld gebeurd is bij de vierkleurenstelling.
Ad 2. Ook informele, door mensen bedachte bewijzen worden steeds complexer en worden slechts door een paar specialisten in de wereld begrepen. Omdat deze resultaten ook elders gebruikt kunnen worden, zou het goed zijn om hier een zeer betrouwbare basis aan te geven. Indien een stuk wiskunde geformaliseerd is, kan de referee zich beperken tot een oordeel over de relevantie. De verificatie-techniek wordt toegepast in de betrouwbare constructie van hardware en software. Dit zou wel eens een van de meest belangrijke toepassingen van de wiskunde kunnen worden.
Ad 3. Het is mogelijk om de geformaliseerde wiskunde zo weer te geven, dat stappen die voor een menselijke wiskundige overduidelijk zijn, uit het zicht blijven. Zo komt de rest vrij goed overeen met de bekende, informele bewijsstijl.
Ad 4. Van de hardware van computers wordt tegenwoordig gedeeltelijk de correctheid bewezen. Voor het operating systeem en de compiler ontbreekt deze geverifieerde betrouwbaarheid inderdaad. Maar omdat het bij de wiskundige assistent (platform plus verificatie-programma) om een product gaat dat door vele mensen gebruikt wordt (reeds nu), zullen ontwerpfouten snel gevonden worden. Men moet dan ook niet spreken van absolute betrouwbaarheid, maar de hoogst mogelijke graad van betrouwbaarheid. Deze ligt altijd nog vele malen hoger dan de resultaten van de informele wiskunde.

Indrukwekkende case-studies (o.a. de Jordancurvestelling, priemgetallenstelling en natuurlijk de genoemde vierkleurenstelling) laten zien dat formaliseren mogelijk is.

Wanneer deze techniek gemeengoed wordt, zullen wiskundigen op een andere manier kunnen communiceren: de focus kan komen te liggen op ideeën en de intuïties erachter. Tenslotte: formaliseren heeft zijn eigen schoonheid. Iedere 21e-
eeuwse wiskundige zou op zijn minst één bewijs op deze manier weergegeven moeten hebben.

Henk Barendregt

Radboud Universiteit Nijmegen