Computerbeweise Auf der Spur des Obststapel-Rätsels

Schon vor Jahren hat ein US-Professor eines der grundlegenden Probleme der Mathematik bewiesen - zumindest ist er davon überzeugt. Doch die überforderte Fachwelt verweigert ihm die Anerkennung. Der Beweis des Beweises bringt nun Mensch gegen Maschine auf.

Von Alexander Stirn


Die großen mathematischen Probleme liegen auf der Straße. Oder am Gemüsestand. Dort wählen die Händler, wenn sie ihre Früchte ebenso ansprechend wie effizient stapeln wollen, die Form einer Pyramide. Die einzelnen Äpfel oder Orangen werden dabei genau über den Mulden der darunter liegenden Schicht platziert.

Mathematiker Hales: Mit Kepler gegen das System
University of Pittsburgh/ CIDDE

Mathematiker Hales: Mit Kepler gegen das System

Schon im Jahr 1609 stellte der Astronom und Mathematiker Johannes Kepler die These auf, dass es sich bei dieser Anordnung um die dichtest mögliche Packung von Kugeln handelt. Knapp vier Jahrhunderte lang bissen sich Mathematiker am Beweis dieser Vermutung die Zähne aus.

Doch vor fünf Jahren überraschte der junge US-Forscher Thomas Hales, heute an der University of Pittsburgh, die Fachwelt mit seinem Beweis. Über zehn Jahre lang hatte er mit Hilfe von Computern mehr als 100.000 Ungleichungen überprüft. "Am Anfang glaubte ich an einen leichten Sieg", erinnert sich Hales gegenüber SPIEGEL ONLINE. "Doch am Ende fühlte ich mich wie ein erschöpfter Marathonläufer, der über die Ziellinie kriecht."

Die Belohnung einer solchen wissenschaftlichen Ausdauerleistung: eine Veröffentlichung in der renommierten Fachzeitschrift "Annals of Mathematics". Normalerweise. Doch Robert MacPherson, einer der Herausgeber der "Annals", zögerte zunächst - wegen der in Mathematikerkreisen nicht gern gesehenen computergestützten Beweisführung. Schließlich setzte der Herausgeber, wie das Wissenschaftsmagazin "Nature" berichtet, statt der üblichen drei gleich ein Dutzend Gutachter auf den Beweis an.

Deren Aufgabe war nicht leicht: Da es sich als unmöglich erwies, jede einzelne Programmzeile zu studieren, mussten die Gutachter die zu Grunde liegenden Gedanken, die Annahmen und logischen Schlussfolgerungen Schritt für Schritt überprüfen.

Vier Jahre später gaben sie auf. Die Experten hatten zwar keinen Fehler gefunden, konnten aber auch nicht zeigen, dass Hales' Beweis hundertprozentig korrekt ist. "Die Nachrichten der Gutachter sind schlecht", habe MacPherson ihm damals geschrieben, erzählt Hales. "Sie werden den Beweis nicht bestätigen können, weil sie einfach am Ende sind."

Protokoll mit 250 Seiten

Kritiker werfen Hales vor, er habe es den Gutachtern alles andere als leicht gemacht. 250 Seiten habe das Manuskript umfasst, als es zur Veröffentlichung eingereicht wurde, fünf Teile mit teils unterschiedlichen Notationen, eher ein Protokoll als ein Artikel. Gegenüber SPIEGEL ONLINE weist der US-Forscher solche Anschuldigungen zurück. "Das mag vielleicht auf die erste Version zutreffen, doch in den letzten Jahren habe ich beträchtlich viel Zeit in ein einfacheres Manuskript gesteckt."

Nach zähem Ringen haben sich die Herausgeber der "Annals" nun offensichtlich entschieden, den Beweis doch zu veröffentlichen - wenn auch unter Vorbehalt. Wie "Nature" berichtet, soll der Artikel vermutlich nächstes Jahr mit einem Vorwort erscheinen, in dem die Herausgeber klar machen, dass sich derartige computergestützte Beweise unmöglich vollständig begutachten lassen. Die Kapitulation der klassischen Mathematik?

Was nach einer Wissenschaftsposse klingt, offenbart einen grundlegenden Disput innerhalb der modernen Mathematik: Inwieweit dürfen Computer den menschlichen Sachverstand ersetzen? Und können die Rechner überhaupt korrekte Beweise führen?

Dank immer besserer Computer können Mathematiker heutzutage deren schiere Rechenkraft für ihre Beweisführung nutzen. Immer neue Lösungen werden berechnet, bis schließlich die korrekte gefunden ist. Traditionell orientierte Mathematiker finden solch ein Vorgehen "anspruchslos". Zudem helfe es nicht, das Problem wirklich zu verstehen und neue Ideen zu entwickeln. Es ist eine Auseinandersetzung Mensch gegen Maschine - und viele Mathematiker, deren Handwerkszeug seit Jahrhunderten Intuition und bestechende Logik sind, beschleicht beim Gedanken an Computerbeweise ein seltsames Gefühl.

Gutachter aus Bits und Bytes

Nicht so Hales. "In hundert Jahren werden Mathematiker darüber staunen, dass einst Beweise auf dem Papier überprüft wurden, genauso wie wir uns wundern, dass früher die Kreiszahl Pi mit der Hand berechnet wurde." Deshalb will der Forscher nun die Beweisführung selbst anpacken - natürlich mit einem Gutachter aus Bits und Bytes.

Der Computer soll zeigen, dass jeder Schritt des Kepler-Beweises korrekt ist - für den Amerikaner nicht nur ein Frage der Ehre, sondern auch des Systems. Hales sieht sich als "Reformer". Das gegenwärtige System belohne einfache Lehrsätze mit einer sofortigen Veröffentlichung. Beweise, die nicht ins gängige Modell passten, behindere es dagegen.

Aus der Frustration heraus sei daher auch das neue Computerprojekt zur Überprüfung des Kepler-Beweises entstanden. Doch das Unterfangen selbst könnte für Hales noch viel frustrierender werden. Trotz der Rechnerhilfe würde ein Mensch allein, so Hales' Berechnungen, 20 Jahre brauchen, um das Projekt abzuschließen. Bislang arbeiteten daran "zwei bis drei Leute", macht sieben bis zehn Jahre.

Beweis der Bienen

In der Zwischenzeit - vom Kepler-Hick-Hack genervt - hat sich Hales an einer anderen Herausforderung versucht: 2000 Jahre lang war die These unbewiesen, dass sechseckige Kacheln der ideale Weg sind, um einen Boden vollständig und mit dem kleinstmöglichen Kachelumfang zu bedecken. Bienen verwenden dieses Prinzip intuitiv beim Bau ihrer Waben, um möglichst wenig Wachs zu verschwenden.

Hales gelang der Beweis in nur sechs Monaten, "und er wurde beinahe unverzüglich zur Veröffentlichung akzeptiert", wie der Professor betont. Allerdings: Für den Beweis der Wabenstruktur hat Hales auch weitgehend auf Computer verzichtet.



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


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