Kugelstapel-Theorie von 1611 Kepler hatte recht

Wie muss man Kugeln schichten, damit der Raum optimal genutzt wird? 1611 formulierte der Astronom Johannes Kepler eine Vermutung - doch erst jetzt hat ein Mathematiker zum ersten Mal einen formalen Beweis vorgelegt.

Von

Kepler vermutete richtig: So lassen sich Kugeln optimal im Raum stapeln.
Andreas Loos / FU Berlin

Kepler vermutete richtig: So lassen sich Kugeln optimal im Raum stapeln.


Kaum zu glauben, wie lange sich Mathematiker bereits mit diesem Problem herumschlagen. 1611 formulierte der Astronom Johannes Kepler die später nach ihm benannte Vermutung: Es gibt eine dichteste Art, Kugeln zu stapeln - nämlich pyramidenförmig, übereinander. Das Volumen ist dann zu etwas mehr als 74 Prozent mit Kugeln gefüllt - mehr geht nicht.

Jeder kennt die dichteste Kugelpackung aus dem Supermarkt: Wenn Orangen zu großen Pyramiden gestapelt werden, geschieht das intuitiv genau wie von Kepler vorgeschlagen. In der ersten Lage bilden drei einander berührende Orangen regelmäßige Dreiecke. Die Orangen der nächsten Schicht werden in die Lücken der Schicht darunter gelegt.

1998 konnte der US-Mathematiker Thomas Hales endlich beweisen, dass Kepler tatsächlich recht hatte. Dabei musste Hales jedoch einen Computer zu Hilfe nehmen, was nicht allen Kollegen schmeckte. Er bekam zu hören: Toll, dass der Beweis per Computer geglückt ist. Aber noch schöner wäre ein "richtiger" Beweis.

Den hat Hales nun nach eigener Aussage vorliegen: "Wir haben unseren Beweis von 1998 mit einer speziellen Software auf logische Konsistenz überprüft", sagt Hales im Gespräch mit SPIEGEL ONLINE. Die Prüfsoftware sei dabei zum Ergebnis gekommen, dass an dem teils klassisch auf Papier und teils am Computer durchgeführten Beweis alles stimme. Im nächsten Schritt müssen nun Kollegen das Ganze überprüfen, danach könnte die Arbeit publiziert werden, und letzte Zweifel am Beweis der Keplerschen Vermutung wären ausgeräumt.

Diese Zweifel waren es auch, die Hales keine Ruhe gelassen hatten. Sein Beweis von 1998 war mehrere Jahre lang von einem Dutzend Mathematikern geprüft worden. 250 Seiten auf Papier und vor allem die Tausenden Zeilen Programmcode brachten die Reviewer jedoch an ihre Grenzen. Der ungarische Mathematiker Gabor Fejes Toth erklärte schließlich, er sei sich zu 99 Prozent sicher, dass der Beweis stimme. Man habe jedoch nicht die Korrektheit aller Computerberechnungen prüfen können.

So entstand das Projekt eines formalen Beweises. Statt eines Reviewers aus Fleisch und Blut sollte ein Computerprogramm jeden einzelnen Schritt des Beweises auf logische Konsistenz checken. Solche Programme werden beispielsweise von Informatikern eingesetzt, um Softwarebugs zu finden. "Der Proof-Checker besteht aus nur 200 Zeilen Code, unser Kepler-Beweis hat mehrere Tausend", sagt Hales.

Können wir Computern trauen?

Der Mathematiker weiß, dass ein per Software überprüfter Computerbeweis Puristen kaum überzeugen dürfte. Angesichts des enormen Code-Umfangs gab es jedoch keinen anderen Weg, so Hales. "Natürlich können sie sagen: Vielleicht hat die Prüfsoftware einen Bug? Wie kann ich ihr trauen?" Die beiden verwendeten Proof-Checker Isabelle und HOL Light stammten jedoch nicht von ihm selbst, betont er. Sie seien mehrfach gecheckt worden - auch durch sich selbst. "Es ist verrückt: Der Code wurde benutzt, um sich selbst zu prüfen."

Eine Aussage, die Logiker aufhorchen lässt. Schließlich hatte Kurt Gödel 1931 mit dem zweiten Unvollständigkeitssatz gezeigt, dass widerspruchsfreie Systeme ihre eigene Widerspruchsfreiheit nicht beweisen können. Nichtsdestotrotz gibt es immer mehr Mathematiker, die Proof-Checker für eine sehr gute Idee halten, weil sie im Zweifel genauer arbeiten als Menschen.

Aus unendlich vielen werden 50 Kugeln

Der eigentliche Beweis von Hales beruht auf einer geschickten Vereinfachung des Packproblems. Am ehesten lösbar wäre die Aufgabe, wenn man so viele Kugeln wie möglich in einen vorgegebenen Behälter legen müsste. Doch damit findet man keine allgemeine Lösung, denn kleine Änderungen an Größe und Form des Behälters beeinflussen die maximal erreichbare Packungsdichte.

"Um den Effekt eines Containers zu eliminieren, muss man eine unendliche Zahl von Kugeln in einem unendlich großen Raum betrachten", erklärt Hales. Man könne aber nur mit einer endlichen Kugelzahl rechnen. Schließlich sei es ihm durch theoretische Betrachtungen gelungen, das Packproblem auf 50 Kugeln zu reduzieren. Dieser Teil des Beweises wurde 2005 in den "Annals of Mathematics" veröffentlicht, an ihm hatten die Reviewer nichts auszusetzen.

Das eigentliche Packproblem wurde dann mit Computerhilfe gelöst. "Wir haben 50 Kugeln. Ihre Anordnung im Raum ist ein kombinatorisches Problem", sagt Hales. 2500 mögliche Fälle seien einzeln untersucht worden, fast alle unregelmäßig. In jedem einzelnen Fall ging es um die Frage, ob die Dichte höher war als von Kepler vorhergesagt. Eine Workstation sei damals drei Monaten lang damit beschäftigt gewesen. Ergebnis: Kepler hatte recht.

Es gibt übrigens eine interessante Anwendung der von Hales beim Beweis genutzten mathematischen Methoden: die Übertragung komprimierter Daten. Dabei sollen so viele Informationen wie möglich transportiert werden, aber es treten auch Störungen durch Rauschen auf. Sind die Signale zu dicht gepackt, bekommt man Fehler. "Die Frage ist: Wie dicht kann ich die Signale packen?", sagt Hales. Dieses Problem sei mathematisch eng mit der Kugelaufgabe verwandt.

Dass er Keplers Vermutung nun wohl endgültig bewiesen hat, erfüllt den Forscher der University of Pittsburgh mit Stolz: "Ein großes Problem, seit Jahrhunderten ungelöst, wer will da nicht der Erste sein?" Er sieht die Arbeit mit dem Proof-Checker auch als Signal an Kollegen. "Ich hoffe, unser Projekt trägt dazu bei, dass immer mehr Mathematiker ihre Beweise per Software prüfen."



Forum - Diskutieren Sie über diesen Artikel
insgesamt 65 Beiträge
Alle Kommentare öffnen
Seite 1
fpwolf 19.08.2014
1. Marktfrau
Dazu hätte es keinen Kepler gebraucht, das weiß die Marktfrau seit Jahrhunderten. Schaut euch mal die Seitenschwerter holländischer Plattbodenschiffe an. Die sind einige Grad zur Fahrtrichtung angestellt, und haben ein asymmetrisches Profil, um einen Druck nach Luv zu erzeugen, als Gegenkraft zum Abtrieb. Das wurde empirisch vor über 200 Jahren erfunden, lange bevor Tragflügelprofile für die Luftfahrt entstanden. Also: für Probleme in der Zukunft ab und zu mal weit in die Vergagngenheit schauen!
Layer_8 19.08.2014
2. Kugelstapler
Zitat von sysopAndreas Loos / FU BerlinWie muss man Kugeln schichten, damit der Raum optimal genutzt wird? 1611 formulierte der Astronom Johannes Kepler eine Vermutung - doch erst jetzt hat ein Mathematiker zum ersten Mal einen formalen Beweis vorgelegt. http://www.spiegel.de/wissenschaft/mensch/keplersche-vermutung-mathematiker-beweist-kugelstapel-theorie-a-986851.html
"Es gibt übrigens eine interessante Anwendungen der von Hales beim Beweis genutzten mathematischen Methoden: die Übertragung komprimierter Daten. Dabei sollen so viele Informationen wie möglich transportiert werden, aber es treten auch Störungen durch Rauschen auf. Sind die Signale zu dicht gepackt, bekommt man Fehler. "Die Frage ist: Wie dicht kann ich die Signale packen?", sagt Hales. Dieses Problem sei mathematisch eng mit der Kugelaufgabe verwandt." Und dies war zum Beispiel ein Anlass, das Problem mit 24-dimensionalen Kugeln anzugehen. Wegen der Farbcodierung der Voyager-Bilder (und deren Komprimierung) vom Sonnensystem. RGB, je 8 Bit sind 24 Bit. Meines Wissens nach wurde die Keplersche Vermutung deswegen zuerst mal so für 24 Dimensionen bewiesen :-)
guitar-junky 19.08.2014
3.
Zitat von fpwolfDazu hätte es keinen Kepler gebraucht, das weiß die Marktfrau seit Jahrhunderten. Schaut euch mal die Seitenschwerter holländischer Plattbodenschiffe an. Die sind einige Grad zur Fahrtrichtung angestellt, und haben ein asymmetrisches Profil, um einen Druck nach Luv zu erzeugen, als Gegenkraft zum Abtrieb. Das wurde empirisch vor über 200 Jahren erfunden, lange bevor Tragflügelprofile für die Luftfahrt entstanden. Also: für Probleme in der Zukunft ab und zu mal weit in die Vergagngenheit schauen!
Es ist das eine, die Lösung zu kennen, aber etwas völlig anderes, das auch zu Beweisen. Das ist in der Mathematik häufig so, dass Sachverhalte, die ansich sehr leicht zu verstehen und zu lösen sind, schwer zu beweisen sind.
Georg_Alexander 19.08.2014
4. Beweis?
Zitat von fpwolfDazu hätte es keinen Kepler gebraucht, das weiß die Marktfrau seit Jahrhunderten. Schaut euch mal die Seitenschwerter holländischer Plattbodenschiffe an. Die sind einige Grad zur Fahrtrichtung angestellt, und haben ein asymmetrisches Profil, um einen Druck nach Luv zu erzeugen, als Gegenkraft zum Abtrieb. Das wurde empirisch vor über 200 Jahren erfunden, lange bevor Tragflügelprofile für die Luftfahrt entstanden. Also: für Probleme in der Zukunft ab und zu mal weit in die Vergagngenheit schauen!
Empirie ist alles andere als ein Beweis. Natürlich weiß jeder aus Erfahrung, dass die Kugeln auf dem Marktstand höchstwahrscheinlich am dichtesten gepackt sind - aber die Herausforderung ist der formale Beweis... Viel Spaß bei diesem scheinbar kleinen Problemchen... (Aber vielleicht sind Sie ja ein Genie ;-)
Bundeskanzler20XX 19.08.2014
5. Talentfrei
Zitat von sysopAndreas Loos / FU BerlinWie muss man Kugeln schichten, damit der Raum optimal genutzt wird? 1611 formulierte der Astronom Johannes Kepler eine Vermutung - doch erst jetzt hat ein Mathematiker zum ersten Mal einen formalen Beweis vorgelegt. http://www.spiegel.de/wissenschaft/mensch/keplersche-vermutung-mathematiker-beweist-kugelstapel-theorie-a-986851.html
Was soll man davon halte, sicher ist es für Mathematiker wichtig eine rechnerische Lösung zu finden. Das ist was sie antreibt! Aber das es die beste Variante ist die Kugeln, so wie im Artikel beschrieben, zu stapeln ist schon mit bloßem Auge sichtbar. So minimiere ich ganz einfach den Raum zwischen den Kugeln auf das Minimum. Würde man Kugel auf Kugel legen errechnet sich die Gesamthöhe aus der Anzahl der Kugeln × Durchmasser. Liegen sie exakt in den Zwischenräumen Überschneiden sich die Durchmesser und so verringert sich die Gesamthöhe und so das Gesamtvolumen einer imaginären Hülle. Bleibt noch zu fragen ob für sowas statliche Forschungsgelder verschwendet wurden?
Alle Kommentare öffnen
Seite 1

© SPIEGEL ONLINE 2014
Alle Rechte vorbehalten
Vervielfältigung nur mit Genehmigung der SPIEGELnet GmbH


Die Homepage wurde aktualisiert. Jetzt aufrufen.
Hinweis nicht mehr anzeigen.