Wie kann man Kugeln stapeln, dass sie möglichst wenig Raum brauchen? Schon 1609 hatte der Astronom und Mathematiker Johannes Kepler diesbezüglich eine Vermutung. Ebenso wie viele Obsthändler: Denn die von ihnen praktizierte Orangenpyramide ist genau eine Variante von Keplers Vision zur Lösung des Problems.

Je einfacher die Praxis, desto schwieriger die Theorie. Fast 400 Jahre mussten vergehen und viele Mathematiker kläglich scheitern. 1998 präsentierte der US-Mathematiker Thomas Hales dann der Öffentlichkeit einen Beweis für die Richtigkeit der Kepler'schen Vermutung. Normalerweise lässt solch ein Ereignis die Sektkorken knallen. Nicht so hier. Der Grund für die Zurückhaltung: Hales verwendete für seinen Beweis einen Computer.

Während in der angewandten Mathematik die Rechenkraft des Computers als Segen gesehen wird, begegnen ihr manche reinen Mathematiker mit Skepsis. Sie beschäftigen sich damit, die mathematische Welt zu bauen, in der sich der angewandte Mathematiker sicher bewegen kann. Eine Welt, die von Gesetzen bestimmt ist, die alle hieb- und stichfest bewiesen werden müssen, bevor sie als solche gelten dürfen. Das war lange Zeit ausschließlich die Sache des mathematischen Kopfes. Bis 1976 Wolfgang Haken und Kenneth Appel den ersten Computerbeweis (siehe Wissen) durchführten und damit ein neues Zeitalter des mathematischen Beweisens einläuteten. Wie eine bis heute währende Diskussion über das Für und Wider. Der zurzeit an der Université Claude Bernard Lyon 1 in Frankreich weilende österreichische Mathematiker Christian Krattenthaler hat gegen Computerbeweise prinzipiell nichts einzuwenden: "Man soll alle zur Verfügung stehenden Mittel benützen, um Fortschritt zu erzielen", so der Kombinatoriker.

Doch müssen die Beweise von unabhängiger Seite überprüft werden können. Gerade das kann zu einem Problem werden. So geschehen bei Hales' Beweis der Kepler'schen Vermutung. Zwölf Mathematiker versuchten vier Jahre lang, im Auftrag des renommierten Fachblattes Annals of Mathematics seine Richtigkeit zu zeigen. Dann gaben sie unverrichteter Dinge auf. Er sei zu 99 Prozent sicher, dass der Beweis richtig sei, eine komplette Zertifizierung sei seinem Team nicht gelungen, so Gabor Fejes-Tóth, Leiter der Bemühungen, in seinem Abschlussbericht. Eine Unsicherheit, mit der die Mathematik lernen muss, zu leben. Und die Puristen längst verfluchen lässt, dass Mathematiker selbst es waren, die den Computer erfunden haben.

Vorteile nicht missen

Aber die negativen Stimmen werden weniger. Viele reine Mathematiker wollen die Vorteile für ihre Arbeit nicht mehr missen. Ihnen dient der Computer nicht nur zum Beweisen, sondern auch als erweiterter Taschenrechner sowie als Quelle der Inspiration. So hat Krattenthaler ein Programm mit dem passenden Namen "Rate" entwickelt, welches eine Formel für eine Folge von Zahlen erraten kann, auch wenn nur ein paar Glieder der Folge bekannt sind. Programme wie "Rate" können helfen, Vermutungen aufzustellen. Ist dann ein Beweis erbracht, nutzt Krattenthaler den Computer auch, um das Ergebnis anhand von Beispielen nachzuprüfen: "Das ist insbesondere bei komplizierten Formeln und Resultaten notwendig, da man sonst nie Sicherheit hat, dass man sich irgendwo auf dem Weg vertan hat."

Mit der Hand wäre das zu aufwändig. Auch der österreichische Mathematiker Bruno Buchberger will seinen Kollegen den Arbeitsalltag erleichtern. Sein Lazy-Thinking-Verfahren findet zu einem mathemati- schen Problem automatisch den Lösungsalgorithmus. Es liefert in Minuten, wofür der Mathematiker Jahre brauchen kann (siehe unten). Die Gefahr, dass sein Verfahren einen Beitrag dazu leistet, Mathematiker um ihr täglich Brot zu bringen, sieht Buchberger nicht. "Es wird immer Problemstellungen geben, für die das Lazy-Thinking-Verfahren den Algorithmus nicht liefert und neue Methoden erdacht werden müssen".

Und dafür braucht es - zumindest noch eine Zeit lang - den Menschen. Thomas Hales liefert einen kleinen Vorgeschmack darauf, welche Dimensionen der reinen Mathematik der Computer als Nächstes erschließen könnte: Er hat - als Reaktion auf das Unvermögen seinen Beweis der Kepler'schen Vermutung vollständig zu überprüfen - ein Projekt mit dem Namen "Flyspeck" ins Leben gerufen. Dessen ehrgeiziges Ziel ist nichts weniger als ein rein formaler Beweis der Vermutung. Bei Hales' Beweis aus dem Jahre 1998 war der Computer noch ein Hilfsmittel. Nun wird er zum Hauptakteur. Der formale Beweis soll aufbauend auf dem 1998er-Original die menschliche Intuition und damit jegliche Unsicherheit eliminieren. Jeder auch noch so kleine Beweisschritt wird mit logischer Strenge durchgearbeitet. Eine Strenge, die kein von einem menschlichen Mathematiker erdachter Beweis liefern kann.

"Flyspeck" startete Anfang 2003. Hales ist mit der Entwicklung zufrieden: "Das Projekt nimmt viel schneller Gestalt an, als ich zu hoffen wagte." Jedoch ist auch hier - wie in der Mathematik so oft - Geduld angebracht. Ob der Gewalt des Beweises ist "Flyspeck" auf 20 Jahre konzipiert. Zumindest sind das bedeutend weniger als 400. (Martina Gröschl, Der Standard, Printausgabe, 13.12. 2004)