Wiskunde / Rekenen met gezond verstand

Quod erat demonstrandum. Met deze woorden sluit de wiskundige zijn bewijsvoering af. Steeds vaker echter moet de logische redenatie plaatsmaken voor de brute rekenkracht van de computer. Maar wie controleert of de computer daarbij geen fouten maakt? Juist, de computer zelf. Dat is even wennen.

Eigenlijk is het een probleem van niks. Elke groenteman weet hoe het moet. Zelfs zonder ooit van Johannes Kepler te hebben gehoord stapelt hij sinaasappelen tot een compacte piramide. Maar de Duitse geleerde bouwde deze stapelmethode in 1611 om tot een wiskundige stelling en poneerde dat het niet compacter kon. Zonder overigens het bewijs erbij te leveren.

Vier eeuwen lang beten wiskundigen hun tanden stuk op het vermoeden van Kepler. Totdat op 9 augustus 1998 Thomas Hales een e-mail de wereld rondstuurde waarin hij beweerde het bewijs rond te hebben. Geïnteresseerden konden alles op zijn internetsite nalezen.

Dat hebben ze geweten. Het bewijs van Hales is niet alleen een wiskundige rekenpartij van 250 pagina's lang, het bevat ook nog een computerprogramma dat met de bijbehorende data 3 gigabyte groot is. Het gerenommeerde vakblad Annals of Mathematics bood aan om het bewijs te plaatsen en zocht er twaalf vakgenoten bij om het te verifiëren -normaal een klus voor hooguit drie zogeheten referees. En ook zij hielden niet van half werk: ze organiseerden zelfs een conferentie waarin ze met collega's bespraken wat de beste aanpak zou zijn.

Maar vijf jaar later gooien de referees de handdoek in de ring. Ze komen er niet uit. Ze weten voor 99 procent zeker dat het bewijs correct is, maar het lukt ze niet de honderd vol te maken. Ze kunnen niet álle computerberekeningen controleren.

Het ziet er nu naar uit dat de Annals het bewijs gaat publiceren, maar met de voetnoot dat de controle niet helemaal is gelukt. Dat zint Hales niet. Want in de wiskunde is 'niet helemaal' hetzelfde als 'helemaal niet'. Zeker als het om een bewijs gaat van een stelling waarvan iedereen toch wel aannam dat hij waar was. Hales wil nu de computer laten aantonen dat zijn bewijsvoering deugt. Dat is niet alleen een hele klus, dat stuit andere wiskundigen weer tegen de borst. Er moet toch een simpeler, traditioneel bewijs te vinden zijn, zeggen zij. Het laatste woord is voorlopig nog niet gezegd.

Het begon allemaal met een eenvoudige vraag van Sir Walter Raleigh. Deze Engelse zeeheld wilde aan het eind van de zestiende eeuw weten hoeveel kanonskogels de gestapelde piramide aan boord van zijn schip bevatte.

Dat was voor zijn wiskundige assistent, Thomas Harriot, een makkie. Hij formuleerde het antwoord wat exacter: Als de bollen netjes laag voor laag worden gestapeld, waarbij in elke laag een bol zes buren heeft en een nieuwe laag in de kuiltjes van de laag eronder terechtkomt, ontstaat er een piramide en nemen de bollen iets meer dan 74 procent van de ruimte in. Harriot vroeg zich ook af of het compacter kon, maar die vraag was voor hem te hoog gegrepen.

Hij legde het probleem aan Kepler voor, maar die wist het ook niet. Hij dácht dat dit de ideale stapeling was, schreef hij dus in 1611, en daar bleef het bij tot 1840. In dat jaar bewees Carl Friedrich Gauss bijna terloops in een boekrecensie dat het vermoeden van Kepler voor regelmatige stapelingen correct was.

Blijven over de onregelmatige stapelingen. Iedereen voelt op zijn klompen aan dat zoiets minder compact moet zijn. Dat kun je ook laten zien: vul een pot met knikkers en de dichtheid is ongeveer 60 procent. Met wat schudden is daar nog 65 procent van te maken, maar dan houdt het op. 74 procent is zo in elk geval onbereikbaar. Maar ja, dat is geen wiskundig bewijs. Men heeft wel geprobeerd het probleem van de andere kant te benaderen en bewezen wat maximale dichtheden zijn. Maar lager dan 77,8 procent is men nooit gekomen.

De enige echte mijlpaal die sinds Gauss in de grond is geslagen, is die van László Fejes Tóth. Deze Hongaarse wiskundige liet in 1965 zien dat de stelling niet voor een oneindig aantal bollen hoefde te worden bewezen; vijftig was genoeg. Daarnaast bewees hij dat de onoverzienbare chaos van oneindig veel bolshopen was terug te brengen tot 5094 soorten stapelingen. Het was een grote stap vooruit, maar destijds kwam je daar niet veel verder mee. Elk type stapeling had zijn eigen niet-lineaire (in lekentaal: extreem lastige) ongelijkheid met 150 variabelen. Om te zien of daaraan is voldaan, heb je een nieuwe generatie computers nodig, merkte Fejes Tóth in 1965 op.

Hier komt Thomas Hales in beeld. Hij hád, begin jaren negentig, die nieuwe computers. Plus de intelligentie en het doorzettingsvermogen om de ongelijkheden van Fejes Tóth om te zetten in voor de computer hanteerbare benaderingen. Zo wist hij er meer dan 5000 te elimineren; de laatste vijftig moest hij 'met de hand' doorrekenen.

Daarmee was zijn bewijs, na meer dan vijf jaar rekenen, klaar. Zijn referees zijn dat echter nog lang niet. ,,Hun probleem is'', zegt de Delftse wiskundige Hans Melissen, ,,dat zij alles wat met computers is gedaan, moeten controleren. En dat kun je alleen door de correctheid van het computerprogramma te bewijzen, of zelf het programma opnieuw te schrijven.''

Melissen denkt dat sommige referees hebben bekeken of het idee, het raamwerk van het bewijs deugt. ,,Maar dat zal wel goed zitten; Hales staat bekend als een gedegen wetenschapper.'' De anderen zitten met de ellende opgescheept. Zij moeten nagaan of alle benaderingen deugen -Hales heeft voor bijna elke ongelijkheid een andere benaderingstruc bedacht- en ze moeten controleren of de computer berekent wat hij moet berekenen, zonder daarbij fouten te maken. En er is eigenlijk maar één manier om dat te doen: alles met de hand nalopen. Maar ja, als dat doenlijk zou zijn, had Hales helemaal niet aan zijn computerklus hoeven beginnen.

Dus houden de referees het hier voor gezien. Maar Hales niet. Hij wil nu de computer zelf inzetten om zijn computergestuurde bewijs te verifiëren. Dat klinkt gek, maar het kan. Er zijn computerprogramma's die wiskundige bewijzen in heel kleine stukjes kunnen hakken. Net zo lang tot elk stukje correspondeert met een bewezen stelling of axioma. ,,In feite gaat het programma met zijn vinger langs het bewijs en controleert het regel voor regel of er geen fouten in zitten'', zegt Freek Wiedijk, informaticus van de KU Nijmegen.

Deze aanpak staat nog in de kinderschoenen. De groep waarvan Wiedijk deel uitmaakt, heeft er onlangs de hoofdstelling uit de algebra (elke veelterm heeft een nuloplossing) mee bewezen, maar het bewijs van Hales is heel andere koek. Het probleem zit hem in het omzetten van het wiskundige bewijs in een voor de computer leesbare vorm. Wiedijk: ,,Hales heeft contact met mij gezocht en ik heb hem toen verteld dat het ongeveer een week werk kost om één pagina wiskunde om te zetten. Zijn bewijs van 250 pagina's is heel compact geschreven. Dat gaat wel acht à tien jaar duren, rekende ik hem voor. Daar schrik ik hem wel mee af, dacht ik, maar Hales werd enthousiast. Hij begreep eruit dat het geen eindeloze missie zou worden.''

De vergelijking met het vierkleurenprobleem dringt zich op. Nog zo'n oude stelling uit de wiskunde. In 1853 vroeg Francis Guthrie zich af hoeveel kleuren je nodig had om willekeurig welke landkaart in te kleuren. Hij opperde dat vier kleuren genoeg waren om te voorkomen dat twee aan elkaar grenzende landen dezelfde kleur zouden hebben.

Niemand die deze simpele bewering kon bewijzen, totdat Appel en Haken in 1977 de botte rekenkracht van een computer gebruikten. Een paar jaar geleden hebben wiskundigen ook een klassiek bewijs geleverd, maar de aardigheid is dat Franse informatici nu claimen dat ze die computeraanpak van het vierkleurenprobleem hebben geverifieerd. Met een computer. Het kan dus wel.

Of niet, want hoe weet je of de computer bij de controle geen fouten maakt? Wiedijk: ,,De kans dat een kromme redenering er door een fout in het computersysteem doorheen glipt, is miniem, te verwaarlozen. Waar het om gaat is dat de computer doet wat je wilt. Het principe dat wij daarbij hanteren, is dat je een kleine kern van je programma moet controleren. De kern waar de hele bewijsvoering doorheen moet. Als je dat vertrouwt, kun je van de rest ook opaan.''

Vertrouwen? Dat is een begrip dat lijkt te vloeken binnen de exacte wiskunde. ,,Het is een kwestie van wennen'', zegt Wiedijk. ,,Ik heb wiskunde gestudeerd en ik was gewend om na het QED (quod erat demonstrandum) het bewijs te checken op denkfouten. Dat hoeft nu niet meer.''

Maar ook de wiskundige Melissen vindt vertrouwen niet zo'n vreemd begrip. ,,Een bewijs dat door referees is goedgekeurd, is een goed bewijs. Totdat iemand laat zien dat het niet deugt. Maar zo lang dat niet gebeurt, vertrouwt iedereen erop dat het correct is.''

Wat wel wringt is de botte bijl van de computer. Veel wiskundigen blijven met het gevoel zitten dat er een beter bewijs moet zijn voor het vermoeden van Kepler, net zoals het bewijs van het vierkleurenprobleem werd verbeterd.

Bovendien is het bewijs de motor van de wiskunde. Niet voor niets daagde David Hilbert in 1900 zijn vakgenoten uit met 23 onbewezen stellingen -Keplers vermoeden zat verpakt in nummer 18. Het idee was dat de uitdagende problemen zouden leiden tot nieuwe wiskunde. Toen Andrew Wiles bijvoorbeeld een paar jaar geleden het laatste theorema van Fermat wist op te lossen, had hij een heel nieuwe tak van wiskunde moeten ontwikkelen. Hales heeft weliswaar knap werk geleverd, maar niets nieuws bijgedragen.

Nu is dat een lot dat de meetkunde wel vaker treft, zegt Melissen. ,,In de getallentheorie is een bewijs vaak een speciaal geval van een heel nieuw gebied, maar in dit soort meetkunde gaat dat minder op. Daar staan bewijzen meer op zich.''

Toch kan ook hieruit nog wat moois voortvloeien. Johannes Kepler stortte zich ooit op de gestapelde kanonskogels omdat hij er een mooie atoomtheorie in zag. Dat geldt nog steeds. En in meer dimensies staat het compact stapelen van bollen gelijk aan het slim verpakken van digitale boodschappen. Zelfs de programma's waarmee de bewijzen worden gecontroleerd, hebben hun nut: eigenlijk zijn ze bedoeld om de correctheid van chips te testen.

Maar bovenal is het de uitdaging van een wiskundig probleem dat eenvoudig aan iedereen is uit te leggen en toch zo moeilijk te bewijzen bleek. Had Hilbert bij de presentatie van zijn stellingen niet gezegd dat een wiskundige theorie pas echt compleet is als je hem aan de eerste de beste voorbijganger kunt uitleggen?

Wat dat betreft hebben de wiskundigen nog een lange weg te gaan. Toen Thomas Hales vijf jaar geleden zijn e-mail rondstuurde, kreeg hij ook een reactie van de plaatselijke veiling: ,,Kunt u meteen hierheen komen? Wij weten wel hoe je sinaasappelen moet stapelen, maar we hebben moeite met de artisjokken.''

Meer over

Wilt u iets delen met Trouw?

Tip hier onze journalisten

Op alle verhalen van Trouw rust uiteraard copyright. Linken kan altijd, eventueel met de intro van het stuk erboven.
Wil je tekst overnemen of een video(fragment), foto of illustratie gebruiken, mail dan naar copyright@trouw.nl.
© 2019 DPG Media B.V. - alle rechten voorbehouden