Je leest:

Computer stapelt sinaasappels

Computer stapelt sinaasappels

Auteur: | 22 juli 2003

In 1998 heeft de wiskundige Thomas Hales met de hulp van computers het vermoeden van Kepler bewezen. Het vermoeden van Kepler is makkelijk uit te leggen – maar razend moeilijk om op te lossen! Kepler zei in 1611, dat de compactste manier om bollen van dezelfde grootte te stapelen, een piramide is. Hij gaf daar echter geen bewijs voor en dus was het aan volgende generaties van wiskundigen om dat te leveren.

Dat bewijs was niet zo makkelijk te leveren. Intuïtief gezien is een pakking als de piramide namelijk erg efficiënt met zijn twaalf buren per bol. Dat heet de face centered cubic packing of FCC-stapeling. Maar wie zegt er, dat er geen speciale onregelmatige stapeling is die nét iets compacter is dan die regelmatige opbouw? Om zeker te weten dat de FFC-stapeling de compactste is, moeten álle andere stapelingen worden doorgerekend.

Elke sinaasappel raakt horizontaal aan zes buren. Elke laag sinaasappels ligt in de holtes tussen de vruchten van de laag eronder. In deze stapeling nemen de bollen 74,048048…% van de ruimte in. Er zijn variaties op deze stapeling, die dezelfde hoeveelheid ruimte innemen. De verzamelnaam voor dat soort stapelingen is face centered cubic packing. bron: Bill Casselman, Universiteit van Britisch Columbia, Canada

Dalende schatting

Vóór Hales heeft niemand ooit kunnen bewijzen dat de FCC-stapeling de hoogst mogelijke dichtheid heeft. Wel is er onderzoek gedaan naar de maximale waarde die die dichtheid kan hebben. In de loop der jaren is de schatting van dat getal steeds gedaald. In 1958 berekende C.A. Rogers nog een waarde van 77,964…%, maar daalde al snel naar 77,844% (Lindsey, 1986) en toen 77,836% (Muder, 1988). Dat ligt allemaal nog ruim boven de 74,048048…% van de FCC. Naast onderzoek naar de theoretische bovengrens probeerde men ook direct te bewijzen dat er geen stapeling bestaat met hogere dichtheid dan de FCC.

In 1993 publiceerde Wu-Yi Hsiang, een wiskundige van de universiteit van Californië in Berkeley, een bewijs van 100 pagina’s van Keplers vermoeden. Grondige controle door experts toonde echter aan dat er gaten zaten in zijn bewijsvoering. Hsiang gelooft niet dat de kern van het bewijs daardoor wordt aangetast, maar de meeste experts denken niet dat zijn artikel een sluitend bewijs van het vermoeden is. Op zijn best, zeggen Hsiang’s collega’s, is het artikel een schets van hoe het bewijs moet worden opgebouwd.

Andere route

Wu-Yi Hsiang gebruikte voor zijn bewijs weinig meer dan een pen, papier en een rekenmachine. In 1965 had de Hongaarse wiskundige László Fejes Tóth laten zien dat je, als je het vermoeden voor 50 bollen kunt bewijzen, je het ook voor oneindig veel bollen hebt bewezen. Verder liet Fejes Tóth zien, dat er maar 5000 verschillende stapelingen meedingen naar de titel van compactste stapeling. Maar de berekening die aangeeft welke stapeling de compactste is, was in 1965 onmogelijk met de hand uit te voeren. Fejes Tóth hoopte dan ook, dat er in de toekomst met computers een poging zou worden gedaan om het vermoeden met de computer te bewijzen.

In 1998 was het dan eindelijk zover. Thomas Hales van de universiteit van Pittsburgh, Pennsylvania, stuurde een e-mail naar vooraanstaande collega-wiskundigen waarin hij zijn bewijs van Keplers vermoeden aankondigde. Hales had voortgebouwd op het werk van Fejes Tóth en had diens 5000 stapelingen samen weten te vatten in 5 brede categorieën – en één buitenbeentje. Door een slimme combinatie van manieren om het gebied dat een bol inneemt wist hij de stapelingen in zijn vijf brede categorieën door te rekenen.

Tom Hales legt tennisballen in de FCC-stapeling. bron: Bob Kalmbach

Het moeilijkste probleem loste Hales echter niet zelf op. Die taak gaf hij aan zijn promovendus, Samuel Ferguson. Het pentahedrale prisma was een serieuze concurrent van de FCC-stapeling en paste niet netjes in de vijf categorieën die Hales had opgezet. Je krijgt dit prisma door drie bollen boven op elkaar te leggen. Twee ringen van elk vijf bollen omcirkelen deze staaf. De tactieken die bij andere stapelingen werkten waren niet goed toepasbaar op dit prisma.

De waarheid zit in de computer

De abstracte wiskunde was maar één deel van het bewijs dat Hales en Ferguson leverden. Minstens zo belangrijk was het computerprogramma dat de twee schreven om het rekenwerk te doen. Dat programma besloeg uiteindelijk zo’n 40.000 regels aan computercode. De in- en uitvoer samen beslaan meer dan 3 gigabytes aan informatie.

Een toenemend aantal wiskundigen maakt bij het op nieuwe stellingen gerichte onderzoek gebruik van computers, ondermeer in de heuristische beginfase van een onderzoek, voor het testen van vermoedens in speciale gevallen, en voor het testen op mogelijke redeneer- of rekenfouten van resultaten waarvoor men een bewijs denkt te hebben gegeven. Maar het programma van Hales en Ferguson is wel een uitzondering in de wiskunde.

Het bewijs van Keplers vermoeden is, mopperen sommige wiskundigen dan ook, een brute kracht-aanpak waar je niets van leert. In een ‘normaal’ bewijs staan interessante denkstappen, die je als inspiratie kunt gebruiken voor ander onderzoek. Domweg alles doorrekenen is geen elegante oplossing, ook al werkt het nog zo goed. Hales’ onderzoek was trouwens niet het eerste dat uitvoerig gebruik maakte van computers. In de jaren 1970 werkten Appel en Haken het zogenaamde vierkleurenprobleem uit met een IBM-360, een computer met 64 kB aan intern geheugen. Niet veel, maar genoeg om aan te tonen dat elke landkaart die je maar kunt bedenken in te kleuren is met vier kleuren. Dat lijkt simpel te bewijzen, maar wiskundigen probeerden het al sinds Francis Guthrie in 1852 opmerkte dat je er niet méér nodig hebt.

Elke platte landkaart die je maar kunt tekenen is met maximaal vier verschillende kleuren in te kleuren. bron: Project aansluiting TUE – VWO, TU Eindhoven

Een gigantisch computerprogramma als dat van Hales, compleet met in- en uitvoer, is veel lastiger te controleren dan een door mensen opgeschreven redenering. Daarom zette Robert MacPherson, een van de redacteurs van de Annals, twaalf controleurs op het bewijs. Meestal zijn drie referees genoeg om de kwaliteit van een bewijs te testen, maar in dit geval was meer mankracht nodig. De leider van het referee-team was niemand anders dan Gábor Fejes Tóth, de zoon van de wiskundige op wiens werk Hales’ bewijs stoelt.

Na bijna vijf jaar heeft het team van experts dat Hales’ artikel controleerde de handdoek min of meer in de ring gegooid. Het artikel wordt waarschijnlijk volgend jaar geplaatst, maar met een opmerking van de redactie dat het stuk niet geheel is gecontroleerd. De referees zijn er voor 99% zeker van dat de bewijsvoering klopt. Veertigduizend regels computercode controleren bleek uiteindelijk toch een te zware opgave. Het team weet nu dat de logica waarop het programma is gebaseerd klopt, maar het is nog wel mogelijk dat er tijdens de uitvoer onverwachte fouten zijn gemaakt. Met de hand is dat nooit te controleren, anders had Hales de berekeningen wel met de hand in plaats van met de computer uitgevoerd. Maar kunnen collega’s er dan wel op vertrouwen dat Hales’ bewijs klopt? De meeste wiskundigen namen al aan dat Keplers vermoeden klopte, dus een onvolledig bewijs zou niet veel meer opleveren dan extra steun voor het vermoeden.

Flyspeck

Voor Hales en Ferguson is het dan ook een tegenvaller dat hun artikel met een kanttekening van de redactie wordt geplaatst. Vandaar dat Hales nu zelf een nieuw project heeft gestart om zijn bewijs formeel te controleren. Formeel bewijzen betekent, het zal niet als een verrassing komen, dat hij een computer wil gaan gebruiken om zijn computerprogramma door te lichten. Hales schat, dat hij zijn bewijsvoering met bestaande programmatuur om wiskundige stellingen te testen binnen twintig manjaren door kan lichten. Zulke programma’s proberen een ingevoerde stelling te controleren door uit een database van bewezen stellingen en axioma’s de nieuwe stelling af te leiden.

Als Hales zijn groep bijeen heeft, gaat project Flyspeck van start. Dat woord (vliegenpoepje) kreeg Hales als antwoord op de zoekactie F*P*K (Formal Proof of the Kepler conjecture). Collega-wiskundigen kijken met argusogen naar het werk van Hales, die volgens hen iets te gek is op computers. Sommigen zijn bang dat de groeiende rol van computers zal leiden tot wiskunde die voor mensen niet meer te bevatten is. Anderen zien in de toenemende kracht van computerprogramma’s juist krachtige hulpmiddelen om stellingen in een redenering te bewijzen. De kracht van menselijke wiskundigen ligt volgens de voorstanders juist in intuïtieve connecties tussen schijnbaar losstaande gebieden van de wiskunde. Juist dat talent betekent volgens hen dat er geen concurrentie maar samenwerking zal ontstaan waarbij beide wiskundigen – mens en computer – elkaar ondersteunen.

Dit artikel is een publicatie van NEMO Kennislink.
© NEMO Kennislink, sommige rechten voorbehouden
Dit artikel publiceerde NEMO Kennislink op 22 juli 2003

Discussieer mee

0

Vragen, opmerkingen of bijdragen over dit artikel of het onderwerp? Neem deel aan de discussie.

NEMO Kennislink nieuwsbrief
Ontvang elke week onze nieuwsbrief met het laatste nieuws uit de wetenschap.