Logik ist Fleißarbeit. Seit Jahrhunderten folgen Mathematiker, wenn sie eine Hypothese beweisen wollen, einem bewährten Verfahren: Sie zerlegen ihre Argumentation in einzelne, aufeinander aufbauende und von jedermann nachzuprüfende Schritte.
Ein Beweis ist erst erbracht, wenn die kritischen Kollegen überzeugt werden konnten, dass alle Glieder der Argumentationskette bereits bewiesen wurden und somit allgemein akzeptiert sind.
Die Stärke der Mathematik ist ihr Gemeinschaftsgefühl - die Überzeugung, mit anerkannten Methoden und auf gemeinsam erarbeiteten Grundlagen zu forschen. Doch genau dieser Konsens ist nun in Gefahr.
Seit Computer verstärkt der Beweisfindung dienen, geraten die Grundfesten der Mathematik ins Wanken. Traditionalisten und Informatiker streiten sich über die Frage: Wann ist ein Beweis ein Beweis?
"Seit Computer erstmals für mathematische Beweise zum Einsatz kamen, sind deren Anwender in der Defensive, sie müssen zeigen, dass unvollkommene Maschinen die reine Mathematik nicht verderben", sagt Thomas Hales von der University of Pittsburgh, einer der Pioniere der Computerbeweise. "Doch mittlerweile wendet sich das Blatt."
Gleich zwei Hypothesen, über denen Mathematiker mehr als 100 Jahre lang erfolglos gebrütet haben, konnten zuletzt mit einem Computer nach- und - abhängig vom Standpunkt - auch bewiesen werden. Eine davon ist das 1852 aufgestellte Vierfarbentheorem.
Es besagt: Jede nur erdenkliche Landkarte kann mit maximal vier Farben koloriert werden, ohne dass dabei zwei aneinander grenzende Länder dieselbe Farbe bekommen. Wird ein hypothetisches Land beispielsweise von fünf anderen Staaten umgeben, kann es selbst in der Farbe rot dargestellt werden. Die umgebenden Länder bekommen dann abwechselnd die Farben gelb und grün.
Der letzte, noch farblose Staat wird schließlich in einer vierten Farbe, etwa in Blau, eingezeichnet. Im Rahmen eines Beweises muss nun gezeigt werden, dass dieses Muster für alle denkbaren Kartenformen gilt und niemals eine fünfte Farbe nötig wird.
Milliarden Rechenschritte
Bereits 1976 verkündeten die Mathematiker Kenneth Appel und Wolfgang Haken von der University of Illinois, sie hätten das Problem gelöst. Doch ihre Argumentation hatte eine gewaltige Schwachstelle: Große Teile des Beweises waren vom Computer durchgerechnet worden, mehr als 1200 Stunden lang, in Milliarden von Rechenschritten - zu viele, um sie jemals von Menschenhand zu überprüfen.
Für mathematische Gralshüter eine nicht hinzunehmende Provokation. Nicht auszudenken, wenn sich von den Programmierern unbemerkt ein Fehler in die Gedankengänge des Computers eingeschlichen hätte.
Diese Unsicherheit will Georges Gonthier nun beseitigt haben. Der Microsoft-Forscher aus dem britischen Cambridge hat den kompletten Beweis des Vierfarbentheorems automatisiert und in eine Sprache gebracht, die von Mensch und Maschine verstanden werden kann.
Das Prinzip heißt formaler Beweis. Während in die herkömmliche Beweisführung immer ein gewisses Maß an Intuition und Erfahrung einfließt ("es sollte klar sein, dass B aus A folgt"), beruht die bereits Anfang des 20. Jahrhunderts entwickelte formale Lösung auf reiner Logik.
Dazu wird jeder noch so kleine Gedankengang eines Beweises in eine Formelsprache übersetzt, die mit wenigen Regeln auskommt. Indem ein Schritt nach dem anderen abgearbeitet wird, baut sich ganz ohne mathematische Eingebung ein Beweis auf - todlangweilig und viel zu aufwendig für den routinierten Mathematiker, ideal für den Computer.
Denn der Rechner führt die unzähligen Programmzeilen nicht nur klaglos aus, er lässt sich dabei auch von einer universell einsetzbaren Überwachungssoftware beobachten, wie Gonthier nun gezeigt hat. Das Programm erstellt ein Protokoll, das von jedem Mathematiker überprüft werden kann.
Kollegen, die der Beweisführung folgen wollen, müssen sich nicht länger auf die Aussage verlassen, das Programm habe schon richtig gerechnet. "Damit haben wir gezeigt, dass Computer bei Beweisen eingesetzt werden können, ohne an mathematischer Strenge zu verlieren", sagt Gonthier.
Dennoch wirkt der Ansatz auf viele Forscher befremdlich. "Mit einem Computer die Arbeit eines Computers zu kontrollieren, erinnert an den Versuch, Feuer mit Feuer zu bekämpfen", meint der Mathematiker Keith Devlin von der amerikanischen Stanford University.
Georges Gonthier sieht darin keinen Widerspruch. "Ob mit einem Computer die Rechnung im Restaurant oder die Arbeit eines anderen Rechners überprüft wird, macht keinen Unterschied." Wichtig für die Glaubwürdigkeit sei nur, dass die Überwachungssoftware bei allen Problemstellungen funktioniere und nicht speziell auf das Vierfarbentheorem zugeschnitten ist. "Die Summe auf dem Taschenrechner ist schließlich auch vertrauenswürdiger als die Zahl auf der Restaurantrechnung."
In den nächsten Wochen will der Microsoft-Forscher seinen Beweis zur Veröffentlichung in einer renommierten Mathematikzeitschrift einreichen. Eine schnelle Antwort erwartet er allerdings nicht: Mit Computerbeweisen haben Fachblätter noch immer ihre Probleme.
Wie langsam die Mühlen der Mathematik mahlen, weiß auch Thomas Hales. Der Pittsburgher Mathematikprofessor hat 1998 - ebenfalls mit Hilfe des Computers - die Keplersche Vermutung bewiesen. Die fast 400 Jahre alte Hypothese besagt, dass Kugeln am Platz sparendsten gestapelt werden können, wenn die obere Kugel in der Vertiefung liegt, die von den vier quadratisch angeordneten Kugeln in der Ebene darunter gebildet wird.
Ein Prinzip, das Obsthändler bei ihren Orangenpyramiden seit Jahrhunderten anwenden. Für seinen Beweis hat Hales das Problem auf rund 100.000 mögliche Kombinationen reduziert und all diese Variationen mit dem Computer durchgerechnet. Übrig blieb nur die Keplersche Form der Obstpyramide.
Ohne lange zu zögern, hat Hales seine Arbeit bei den Annals of Mathematics eingereicht, der angesehensten Fachzeitschrift auf dem Gebiet der Mathematik. Im Herbst dieses Jahres soll sie nun endlich veröffentlicht werden. Grund für die Verzögerung: Kein Gutachter konnte - wie ansonsten bei wissenschaftlichen Veröffentlichungen üblich - den Beweis von vorne bis hinten überprüfen.
Deshalb soll die Arbeit nun mit einem unkonventionellen Nachsatz veröffentlicht werden, wie Peter Sarnak, einer der Herausgeber der Annals, dem Economist bestätigte. Darin wird lapidar vermerkt: Die Computerprogramme, die zusammen mit dem Beweis eingereicht wurden, können nicht verifiziert werden.
Es wird nicht das letzte Mal sein, dass die Herausgeber der Fachzeitschrift mit solchen Problemen konfrontiert werden. Sarnak rechnet damit, dass in den nächsten Jahren deutlich mehr Artikel mit Computerbeweisen eingereicht werden. Mathematik könnte "ein bisschen wie Experimentalphysik" werden: Neue Erkenntnisse werden erst anerkannt, wenn sie von einem unabhängigen Forscherteam reproduziert wurden.
Die alte Schule zittert
Um das zu umgehen, will auch Hales seinem Kepler-Beweis eine formale, unangreifbare Struktur geben: Das Projekt heißt "Flyspeck", und weltweit sind Mathematiker daran beteiligt. "Bis zum formalen Beweis werden sicherlich noch Jahre vergehen, aber die ersten Ergebnisse sind viel versprechend."
So konnte im Januar der Jordansche Kurvensatz formal bewiesen werden, eine wichtige Voraussetzung für die Keplersche Vermutung. 44.000 Beweisschritte waren dafür nötig, niedergeschrieben in 59.000 Zeilen Programmcode und überwacht von einem Computerprogramm.
Hales hofft, damit auch die Herausgeber der Annals überzeugen zu können. "Das automatisierte Prüfverfahren liefert den höchsten Grad an Zuverlässigkeit, den moderne Technologie garantieren kann - und ist dem Menschen deutlich überlegen."
Verglichen mit dem alten Gutachterverfahren bei Fachzeitschriften und den damit verbundenen menschlichen Fehlern, seien Computer um viele Größenordnungen zuverlässiger. "Das ist fast wie bei der Entfernungsmessung: Früher haben die Menschen Schritte gezählt, heute wird mit Lasern und Atomuhren gemessen."
Verfechter der alten Schule hören das gar nicht gerne. Dass der Computer - wie in fast allen anderen wissenschaftlichen Disziplinen - mittlerweile zum alltäglichen Werkzeug der Mathematiker geworden ist, können jedoch auch sie nicht verhindern. "Mittlerweile scheinen Computer tatsächlich unverzichtbar zur Überprüfung ihres eigenen Beweises geworden zu sein", sagt Keith Devlin. "Die Mathematik wird nie mehr so sein, wie sie einmal war."