Het Keplerprobleem, 400 jaar na dato alsnog bewezen?

In 1998 maakte Thomas Hales bekend dat hij de bijna 400 jaar oude voorspelling van Johannes Kepler over fcc-stapelingen bewezen had. Deze bekendmaking trok wereldwijd veel publiciteit en belandde op de voorpagina's van vele kranten. Een grote groep experts zijn die belast zijn met het zorgvuldig verifiëren van het bewijs geloven dat het daadwerkelijk correct is. Toch is het nog altijd niet gepubliceerd in het prestigieuze tijdschrijft Annals of Mathematics. Het probleem is namelijk dat het bewijs dermate complex is dat het onmogelijk is uit te sluiten dat het bewijs toch nog een klein foutje bevat.

Eén voor één stapelen, het fcc-kristal.

Probeer zoveel mogelijk harde bollen in een doos te passen. Op welke wijze moet je de bollen dan stapelen? De meest efficiënte aanpak is bollen stapelen op een regelmatige manier. Dit is heel veel werk, maar het is wel de beste manier om de ruimte te vullen. Wanneer we dit goed doen, krijgen we een plaatje zoals in figuur 2. Er wordt in het artikel Welke deeltjes stapelen het beste? uitgebreid ingegaan op de theorie erachter.

Thoma Hales

Om het Keplerprobleem wiskundig te bewijzen heeft Hales gebruik gemaakt van de computer. Dit is volgens Hales de enige mogelijkheid, omdat de vergelijkingen die een rol spelen dermate ingewikkeld zijn dat het niet meer op papier is uit te schrijven. Een mens kan nauwelijks meer met deze ingewikkelde formules uit te voeten, maar voor een computer zijn deze extreem complexe formules geen probleem. In het geval van het Kepler probleem gaat het om het bewijzen van over de 100 000. Bij elkaar heeft dit al meer dan 10 jaar tijd gekost. Wiskundigen zijn door deze methode in twee kampen verdeeld. De voorstanders van deze methode vinden dat het gebruik van de computer om stellingen te bewijzen de wiskunde van de toekomst is. De tegenstanders vinden dat deze methode niet elegant is en te weinig inzicht verschaft. Een ander probleem is dat een computerprogramma altijd een fout kan bevatten waardoor de uitkomst onjuist kan blijken te zijn.

Bewijs of geen bewijs? That's the question...

Om zijn gelijk te halen heeft Hales in januari 2003 het zogenaamde Flyspeckproject gestart. In dit project worden geen mensen gebruikt om het bewijs en bijbehorende computerprogramma te controleren op fouten, maar wederom de computer. Het idee is om het bewijs regel voor regel uit te schrijven in zogenaamde axioma's waarvan we weten dat ze correct zijn. Als het volledige bewijs in deze axioma's kan worden herschreven, moet het wel correct zijn. Zelf schat Hales dat dit 20 manjaren gaat kosten. Waarschijnlijk zal het bewijs van Hales eind 2003 toch worden gepubliceerd in het tijdschrift Annals of Mathematics. Hierbij zal de editor van het tijdschrift een (hoogst ongebruikelijk) kort bericht toevoegen dat het onmogelijk was om alle aspecten van het bewijs op juistheid te controleren.