Gesundheit : Der bessere Rechner

Der Computer dringt in das Hoheitsgebiet der Mathematik vor: Er führt Beweise und löst uralte Probleme

Thomas de Padova

Tom Hales ist sauer. Er fühlt sich um seinen Ruhm gebracht. Er hat ein mathematisches Glanzstück vollbracht und einen Beweis vorgelegt, an dem sich Wissenschaftler 400 Jahre lang die Zähne ausgebissen haben: die Keplersche Vermutung. Sie besagt, dass die beste Art und Weise, Kugeln Platz sparend übereinander zu stapeln, eine Pyramide ist.

Was jeder Obsthändler intuitiv richtig löst, wenn er Äpfel und Orangen stapelt, ist für die Forschung eine harte Nuss. Hales hat sie geknackt. Aber seit sechs Jahren wartet er nun schon darauf, dass seine Arbeit in den „Annalen der Mathematik“ veröffentlicht wird.

„Die Verzögerungen waren für mich ein Quell ständiger Frustration“, sagt der Mathematiker der Universität Pittsburgh. Er weiß nicht, wie viel Zeit sich die Gutachter noch lassen werden. Der Grund dafür: Er hat für sein Beweisverfahren massiv Computer eingesetzt. Dass er damit an den Fundamenten der Mathematik gerüttelt hat, ist ihm inzwischen schmerzlich bewusst geworden.

„Es ist nicht der Siegeszug für computergestützte Beweise geworden, der es hätte werden sollen, sondern, im Gegenteil, ein schwerer Rückschlag“, sagt er. „Und es ist eine Warnung an die gesamte Gemeinschaft, dass man es sich als Mathematiker zweimal überlegen sollte, ehe man den Computer für etwas anderes als für Surfen oder für E-Mails einsetzt.“

Drastische Worte. Aber sie treffen einen wunden Punkt. Der Beweis ist der Grundpfeiler der Mathematik. Er garantiert, dass das mathematische Wissen absolut verlässlich ist. Jeder mathematische Beweis muss daher von mehreren Wissenschaftlern überprüft werden.

Die mathematische Gemeinschaft aber sieht sich dazu immer öfter außerstande. Sei es, weil die Beweise zu komplex geworden sind – oder aber weil sie auf einem Einsatz großer Computer beruhen. Und dann gibt es inzwischen sogar Beweise, die der Computer quasi auf Knopfdruck führt.

Er ist Mathematikern längst eine große Hilfe. Ein bekanntes Beispiel hierfür ist das Vierfarbentheorem. Dabei geht es darum, wie viele Farben man mindestens braucht, um eine Landkarte so einzufärben, dass benachbarte Länder immer verschiedenfarbig sind. Die Antwort darauf, dass es, wie vermutet, vier Farben sind, fanden Kenneth Appel und Wolfgang Haken von der Universität Chicago, nachdem sich Mathematiker 120 Jahre daran versucht hatten. Doch bis sie das Problem lösen konnten, waren mehr als 1000 Stunden Rechenzeit ihres Computers und viele Jahre Arbeit verstrichen.

„Wir wissen jetzt, dass es stimmt“, sagt Wolfgang Rautenberg, emeritierter Mathematiker der FU Berlin. „Und wir könnten versuchen, dies jetzt auch anders zu beweisen. Aber das wird vermutlich nicht gelingen. Jedenfalls nicht ohne eine riesige Zahl von Fallunterscheidungen.“ Und die könne man doch, bitteschön, getrost dem Computer anvertrauen.

Rautenberg gehört zu den Mathematikern, die sich mit dem Computer in vieler Hinsicht angefreundet haben. Neben ihm auf dem Schreibtisch etwa liegt ein Minirechner, der auch Astronauten als Notfallinstrument dient. Rautenberg schreibt nebenbei Softwareprogramme für solche Geräte – unentgeltlich.

„Ich habe nun 40 Jahre mathematische Forschung hinter mir“, sagt er. „Es ist ein ständiger Kampf. Wir müssen uns durch Dickichte schlagen, geraten auf Irrwege. Manche geben dabei auf. Das ist kein leichter Beruf. Die Probleme halten einen gefangen, man findet nachts keinen Schlaf, arbeitet das Wochenende durch. Es bedeutet einen Verzicht auf freie Zeit in unglaublichem Maße.“

Dann kommt er auf Hales und dessen Beweis der Keplerschen Vermutung zu sprechen: „Es war zu erwarten, dass so etwas eines Tages passieren würde.“ Vier Jahre lang hatten zwölf Gutachter unter Leitung des ungarischen Mathematikers Gabor Fejes Tóth damit zugebracht, die Beweisführung zu überprüfen, ehe sie erschöpft aufgaben. Toth erklärte schließlich, dass er zu 99 Prozent überzeugt sei, dass das Verfahren richtig sei. Aber mit letzter Sicherheit könne er es nicht sagen.

Damit sei eine Situation entstanden, deren Folgen man nicht abschätzen könne, sagt Rautenberg. Denn die genaue Reproduktion eines Beweises sei nun einmal das A und O der Mathematik.

Eine Frage ist: Kann der Computer auch die Aufgabe der Überprüfung künftig übernehmen? Das jedenfalls ist das Ziel, das sich Hales mit seinem Projekt „Flyspeck“ gesetzt hat: Da es seine Kollegen nicht fertig bringen, sollen nun wiederum Computer jeden Schritt des Beweises der Keplerschen Vermutung kontrollieren. Doch der streng formalisierte Beweis wäre derart umfangreich, dass Hales das Projekt auf 20 Jahre angesetzt hat.

In weniger schwierigen Fällen wird der Computer bereits seit einigen Jahren mit solchen Aufgaben betraut. Zum Beispiel um nachzuweisen, dass Computerprogramme für die Raumfahrt oder das Militär absolut fehlerfrei sind. Das überprüft der Rechner mittlerweile nicht mehr anhand einzelner Fallbeispiele. Er führt stattdessen einen strengen Beweis, der für alle nur denkbaren Fälle gilt. Ein Gegenbeispiel zu finden, ist dann per se ausgeschlossen.

Es sei dem Computer inzwischen in Hunderten von Fällen gelungen, mathematische Probleme quasi alleine zu lösen, sagt Wolfgang Bibel, Mathematiker und Informatiker an der TU-Darmstadt. Aber nur einer sei bislang wirklich Aufsehen erregend gewesen: der Beweis des „Robbins-Problems“ aus der Algebra durch ein Programm, das Bill McCune vom Argonne National Laboratorium bei Chicago und sein Team geschrieben hatten.

„Das Problem konnte 60 Jahre lang einfach niemand lösen“, sagt Bibel. „Das ist in der Mathematik eine lange Zeit. Und dann kommt eine Maschine, die nur logisch denken kann, und löst das Problem innerhalb von ein paar Tagen Rechenzeit.“ Man halte die Mathematik immer für die Königin der Wissenschaften. „Aber das hat die Maschine getoppt! Das war für mich ein viel größeres Ereignis, als wenn ein Computer den Weltmeister im Schach schlägt. Von den intellektuellen Anforderungen her liegt das für mich eine Ebene höher.“

Beweise sukzessive dem Computer zu überlassen, bedeutet allerdings, den Formalisierungsgrad der mathematischen Sprache auf die Spitze zu treiben. Man muss dazu alle anschaulichen Bezüge aus der Mathematik strikt entfernen und darf nur noch eindeutig definierte Begriffe verwenden, die jeglicher Intuition entbehren.

Mit einer solch starren Form aber komme man nicht weit, sagt Raul Rojas, Mathematiker und Informatiker der FU-Berlin. „Denken Sie zum Beispiel an ein geometrisches Problem, dass der Mathematiker plötzlich nicht mehr geometrisch betrachtet, sondern algebraisch. Und mit einem Mal lösen sich alle Schwierigkeiten in Wohlgefallen auf.“ Der Computer könne nicht so einfach eine andere Sichtweise annehmen. „Beim maschinellen Beweisen fehlt das Aha-Erlebnis, das der Mensch hat.“

Die Angst, dass Mathematik in absehbarer Zeit nur noch von Maschinen betrieben werde, sei unbegründet, urteilt Christoph Benzmüller. Er koordiniert an der Universität des Saarlandes das europaweite Forschungs- und Trainingsnetzwerk „Calculemus“, in dessen Mittelpunkt neuartige Software und Computerbeweise stehen. Bei den Computerbeweisen gebe es bislang kaum mehr als Einzelerfolge, sagt er.

Dennoch ist der Computer zweifellos weiter auf dem Vormarsch in ehemals mathematisches Hoheitsgebiet. „Es wäre heute kein Problem mehr, eine Maschine zu bauen, die innerhalb von drei Jahren das Abitur in Mathematik machen könnte“, sagt Bibel.

In Deutschland geschehe auf diesem Gebiet jedoch wenig. Die meisten seiner Kollegen verteidigten ihr Terrain vehement. Sie lehnen den Computer als Beweisinstrument ab oder nehmen ihn nicht ernst. Und sie wehren den Anfängen, wie am Fall Hales deutlich wird.

Als Handlanger des Computers sieht hier zu Lande niemand seine Zukunft. „Wir wollen als Mathematiker unseren Spaß behalten", sagt Bibel. „Und Mathematik zu betreiben, ist ein Spaß.“

0 Kommentare

Neuester Kommentar