1: De QED-utopie
2: Een voorbeeld
In tegenstelling tot wat je misschien zou verwachten, gebruiken wiskundigen computers nauwelijks om hun 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 kijken hoe speciale gevallen van hun stellingen zich gedragen), maar ze gebruiken ze niet om bewijzen mee te controleren. Wiskundige bewijzen zitten in mensenhoofden of zijn opgeschreven in mensentaal, en tot nog toe zijn ze bijna nooit zo opgeschreven dat er geen menselijk begrip nodig is om ze te kunnen nalopen.
In 1994 publiceerde een anonieme groep wiskundigen en informatici het QED Manifesto. 'QED' is de afkorting van 'Quod Erat Demonstrandum' ('dat wat bewezen moest worden'), traditioneel de manier om een bewijs af te sluiten. In het QED Manifesto wordt een toekomst beschreven waarin alle wiskundige bewijzen in de computer zijn gecodeerd. De QED utopie - een wereld waarin de computer wiskundige bewijzen routinematig op correctheid controleert - is het onderwerp van een aantal onderzoeksprojecten. Deze projecten hebben hun doel nog niet bereikt, maar in Nijmegen werkt een groep onderzoekers die hopen dat dat binnenkort zal veranderen.
Automath en zijn opvolgers
De pionier van het formaliseren (het met de computer wiskundige bewijzen controleren) is de Nederlander prof. N.G. de Bruijn. Hij leidde in de jaren zeventig in Eindhoven het Automath project. 'De Automath' was zijn naam voor een machine die voldoende precieze wiskundige bewijzen kan begrijpen. In die tijd dachten de meeste wiskundigen dat het volkomen onpraktisch zou zijn om interessante bewijzen op een dergelijke manier in volledig detail uit te werken. Maar prof. De Bruijn heeft als eerste laten zien dat dat wel degelijk kan!
Er zijn tegenwoordig een vijftiental serieuze systemen voor verificatie van wiskunde. De opvolger van Automath is het Franse systeem Coq. Dit systeem is ontworpen voor bewijzen over computerprogramma's (dus niet primair voor wiskundige bewijzen), en is soms wat onhandig omdat het werkt met een beperkt soort wiskunde dat intuïtionisme heet, maar het kan ook voor echte wiskunde gebruikt worden. In Nijmegen wordt Coq geschikter gemaakt voor echte wiskunde. Om uit te vinden wat voor verbeteringen er daarvoor aan Coq nodig zijn, vertalen ze daar een aantal niet-triviale bewijzen in de Coq taal.
Een systeem dat wél gemaakt is voor wiskunde, is het Poolse systeem Mizar ('Mizar' is de naam van een ster uit het sterrenbeeld de Grote Beer). Dit systeem stamt niet van Automath af, maar is onafhankelijk in de jaren zeventig ontwikkeld. Jarenlang is dit systeem eigenlijk nauwlijks in het westen bekend geweest, maar al die tijd hebben de Polen (en een groep Japanners) bewijzen in de Mizar taal zitten vertalen. Inmiddels heeft de Mizar bibliotheek met gecodeerde wiskunde een indrukwekkende omvang. Het bewijst veertigduizend uitspraken en is ongeveer anderhalf miljoen regels lang.
1 | 2 | next
|
