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 eens aantonen dat het bewijs waterdicht is, blijkt nóg moeilijker. De Nederlander N.G. 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.
Bewijsverificatie met de computer
In 1967 startte de Nederlandse wiskundige N.G. de Bruijn in Eindhoven het Automath-project. Hiermee werd hij een pionier op het gebied van het met de computer verifiëren van wiskundige theorievorming. Dit werk leverde hem in 1985 de Snelliusmedaille op. Automath is gebaseerd op de zogenaamde getypeerde lambda calculus.
In een terugblik op het Automath-project merkt De Bruijn op: “Het Automath-systeem heeft nooit de pretentie gehad om het bedenken van wiskunde te automatiseren, en zelfs niet om de constructie van bewijzen van gegeven stellingen te automatiseren. De Automath-correctheids-checker is niets meer of minder dan een uiterst zorgvuldige lezer van goed-gepresenteerd voltooid wiskundig materiaal.”
Intussen zijn bewijsassistenten, programma’s die bewijzen kunnen verifiëren en die ook (in beperkte mate) kunnen helpen bij het vinden van bewijzen, veel op internet te vinden. The Coq proof assistant is zo’n programma. Met behulp van Coq kun je interactief (in interactie met het systeem) bewijzen ontwikkelen. De laatste puzzelstukjes van het bewijs van het beroemde ‘Vierkleurenprobleem’ werden in 2004 gelegd met behulp van Coq.
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.
Wetenschapsagenda
Een deel van dit artikel is afkomstig uit de Nederlandse Wetenschapsagenda van de Koninklijke Nederlandse Akademie van Wetenschappen (KNAW). Hoe zien de grote wetenschappelijke uitdagingen er nu uit en, vooral, op welke terreinen kunnen Nederlandse onderzoekers een belangrijke bijdrage leveren? De Wetenschapsagenda is een overzicht van uitdagende wetenschappelijke vragen en thema’s, waar de Nederlandse wetenschap een grote bijdrage aan kan leveren.
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.
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.
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.