Streven computers straks zelfs wiskundigen voorbij?

Het bedenken van een nieuw wiskundig bewijs is nog voorbehouden aan een creatief brein. Maar controleren of een wiskundig bewijs klopt, daarvoor zijn al computerprogramma’s ontworpen. Inmiddels worden bewijzen echter zó ingewikkeld dat ze door mensen niet meer te toetsen zijn. Slagen computers straks waar wiskundigen nu zelf nog falen?

Elke groenteboer weet hoe hij zoveel mogelijk sinaasappelen in een kistje krijgt. Maar wiskundig bewijzen dat deze ‘sinaasappelstapeling’ echt het meest efficiënt is, dat valt lang niet mee. Vervolgens ook nog bewijzen dat het bewijs waterdicht was, dat is nóg moeilijker.

De Nederlander Dick de Bruijn was in 1968 de belangrijkste pionier bij het ontwerpen van ‘bewijsassistenten’ – computerprogramma’s die kunnen helpen bij het controleren van een wiskundig bewijs. De pioniers zetten fundamentele bewijsstappen, door wiskundigen in hun hoofd gemaakt, om in een voor computers begrijpelijke, logische taal. Eenmaal voltooid liep de bewijsassistent alle stappen van een bewijs na en controleerde of ze voldeden aan de logische regels. Klopte er iets niet, dan gaf het programma aan wat er mis ging, en waar.

Ivonne Wierink© Ivonne Wierink

Sindsdien hebben Nederlandse wiskundigen en logici, samen met collega’s in het buitenland, het pionierswerk voortgezet. Ze creëerden nieuwe logische talen en verzamelden tal van oude bewijzen van stellingen, die ze gebruikten om bewijsassistenten sneller en slimmer te maken.

Inmiddels hebben computerprogramma’s al meer dan tachtig van de honderd ‘mooiste’ wiskundige bewijzen gecontroleerd. Van die tachtig bewijzen hadden wiskundigen zelf ook al vastgesteld dat ze absoluut klopten. In de wiskunde is dat belangrijk: het bewijs voor een stelling geldt voor de eeuwigheid.

Honderd procent

Tot nu toe doen bewijsassistenten dus wat mensen ook kunnen – ze doen het alleen sneller en zien nooit een foutje over het hoofd. De vraag is of we assistenten kunnen ontwerpen voor bewijzen die te groot en te ingewikkeld zijn geworden voor het menselijk brein – zoals het bewijs dat de groenteboer zijn sinaasappelen optimaal stapelt.

Het bewijs voor de sinaasappelstapeling werd in 1998 door wiskundigen geleverd. Daarna waren twaalf collega-wiskundigen vier jaar bezig om te controleren of het correct was. Zelfs na die vier jaar wisten ze het echter nog niet helemaal zeker. Ze zijn er 99 procent zeker van dat het bewijs klopt – maar wiskunde is onbarmhartig en eist honderd procent.

Een computerprogramma dat zou slagen waar mensen falen, zou iets nieuws toevoegen aan de wiskundige wetenschap.

Voor wiskundigen en logici is dat een intrigerend vooruitzicht, maar bewijsassistenten hebben meer in petto dan het fascineren van wetenschappers. Het met honderd procent zekerheid controleren van een logisch systeem kan bijvoorbeeld ook worden gebruikt om ontwerpen voor computerhardware en -software foutloos te maken.

In 1994 verloor chipfabrikant Intel veel geld door een fout in de Pentium-rekenprocessor. Om te voorkomen dat zoiets opnieuw gebeurt, gebruikt het bedrijf nu een computerprogramma. Ook de chips in de iPod en veel mobiele telefoons zijn door computerprogramma’s gecontroleerd.

Een mathematisch bewijs voor honderd procent controleren, dat was tot nu toe exclusief weggelegd voor wiskundigen. Het wachten is op het moment dat computers het beter kunnen dan zij.