Dichter als hier auf dem Markt in Zagreb, Kroatien, kann man runde Früchte nicht stapeln. Das vermutete Kepler schon 1611. Aber erst 1998 gelang es Thomas Hales, diese "Kepler'sche Vermutung" mithilfe eines Computerprogramms zu beweisen.
aus nzz.ch, 29.7.2015, 05:30 Uhr
Computer als Beweis-Assistenten
Supermathematiker aus Silizium
Die Frage, ob man beim Beweisen von mathematischen Sätzen Computer zur Hilfe nehmen soll, entzweit Mathematiker. Die Kontroverse rührt an die Wurzeln der mathematischen Wahrheit.
von Eduard Kaeser
Sätze der Mathematik gelten als Ausbund reiner und ewiger Wahrheit. Gottfried Benn hat das in seinem berühmten Wort so ausgedrückt: «(Es) gibt nur zwei verbale Transzendenzen: die mathematischen Lehrsätze und das Wort als Kunst. Alles andere ist Geschäftssprache, Bierbestellung.»
Festmahl für einen Beweis
Garant für die mathematische Wahrheit ist der Beweis. Die Entdeckung dieser deduktiven Macht erschien den alten Griechen wie ein Blitzschlag aus dem Götterhimmel. Der Beweis braucht einfache technische Hilfsmittel, einen Schreibstift und ein Stück Papier, um Symbole darauf zu kritzeln – alles andere ist Sache des menschlichen Ingeniums. Pythagoras war derart beeindruckt von seinem Satz und dessen Beweis, dass er der Legende nach ein Festmahl zelebriert haben soll, in dem den Göttern hundert Ochsen geopfert wurden. Die Tradition, die er begründete (nicht der Festschmaus), dauert bis heute an: Sätze, hinter die sich das Signum «quod erat demonstrandum» setzen lässt, sind die unerschütterlichsten Wahrheiten der Menschheit.
Diese Sicht sieht sich schon seit einiger Zeit herausgefordert – an der logischen und an der technischen Front. Um die Wende vom 19. zum 20. Jahrhundert entdeckten die Logiker Widersprüche in den konzeptuellen Fundamenten der Mathematik. Eine Mathematik aber, deren Grundlage nicht solide ist, ist unbrauchbar. Aus ihr liessen sich auch Sätze wie «1=2» beweisen.
Einen Weg, die Mathematik von Grund auf zu reparieren, sah man darin, mathematische Sätze in Sätze eines formalen Systems zu übersetzen. Eine perfekte Beweis-Maschine würde dann überprüfen, ob ein eingegebener gültiger Satz im System auch aus dessen Axiomen beweisbar sei. Aber Kurt Gödel wies nach, dass man die Hoffnungen in die Vollständigkeit einer solchen Maschine zurückschrauben muss: Sie liefert nicht einmal für alle eingegebenen wahren Sätze der Arithmetik einen Beweis.
Nun scheint es, als hätten die Mathematiker in den Computeralgorithmen eine neue derartige Maschine entdeckt. Die Maiausgabe des amerikanischen Wissenschaftsmagazins «Quanta» brachte einen Artikel mit dem Titel «Werden Computer die Wurzeln der Mathematik neu definieren? »; 2013 fragte ein Titel im gleichen Magazin sinnig « In Computers We Trust? »; und der renommierte Wissenschaftsjournalist John Horgan liess schon 1993 im «Scientific American» ein Fanal ertönen: « The Death of Proof ».
Fermats Vermutung
Nüchtern betrachtet handelt es sich um einen Trend oder Stil in der mathematischen Beweisführung, der sich immer mehr auf die Dienste des Computers abstützt. Die geniale Einfachheit des pythagoreischen Beweises bezaubert einen heute noch. Der Beweis eines allgemeineren Satzes aus der pythagoreischen Tradition, nämlich des letzten Satzes von Fermat, ist da schon viel schwieriger. Das mathematische Rätsel, das Pierre de Fermat beschäftigte, lautet: Gibt es drei ganze Zahlen a, b und c, welche die Gleichung an+bn=cn für n grösser als 2 erfüllen? Wie man sogleich sieht, fand Pythagoras eine Lösung für n=2. Und wie Fermat vermutete, lautet die Antwort auf die allgemeine Frage: Nein. Aber erst über drei Jahrhunderte später gelang Andrew Wiles ein Beweis der Fermatschen Vermutung.
Wiles Arbeit manifestiert exemplarisch die ganze Problematik des modernen Beweises. Er wird immer babylonischer. Wiles brauchte über 200 Seiten zur Formulierung. Er bediente sich der herkömmlichen deduktiven Methode über viele Hilfssätze, arbeitete in eremitischer Klausur. Eine erste Version des Beweises stellte sich als lückenhaft heraus. Und hier zeigt sich die Ironie: Nur schon der Nachvollzug des Beweises ist eine vertrackte Aufgabe für sich. Das Gerücht kursiert, etwa einer von tausend Mathematikern sei fähig, den Beweis zu evaluieren. Man muss sich das in aller Klarheit vergegenwärtigen: Ein Mathematiker beweist einen fundamentalen Satz, und kaum einer seiner Zeitgenossen kann das «quod erat demonstrandum» nachvollziehen. Man glaubt ihm einfach, oder man glaubt ihm nicht.
Sekundanten des Geistes
Und es ist durchaus der Geruch eines Glaubenskriegs zwischen Klassikern und Modernisten, welcher der Kontroverse um die Einführung des Computers anhaftet. Der menschliche Geist hat sich in der Mathematik ein schier unendliches Reich eröffnet, dem er ironischerweise nicht gewachsen ist – Benns «Transzendenz». Deshalb machen Befürworter des computerisierten Beweises geltend, dass der menschliche Geist durch den maschinellen sekundiert werden müsse. Als Folge davon zählt nicht mehr die absolute Korrektheit, sondern die experimentell und rechnerisch bestätigte Glaubwürdigkeit.
Der Informatiker Robert S. Boyer publizierte in den 1990er Jahren das sogenannte QED-Manifest (von «quod erat demonstrandum»). Es propagiert eine Idee, die direkt der Phantasie eines Jorge Luis Borges entsprungen sein könnte, nämlich den gesamten mathematischen Korpus – inklusive bewiesener und unbewiesener Theoreme – in einer einzigen Datenbank zu komprimieren. Eine solche Datenbank, so Boyer, würde den Nutzern ermöglichen, das mathematische Wissen nach relevanten Resultaten und Hinweisen abzusuchen, und auf einer solchen Basis würde man mithilfe der Tools von QED glaubwürdige Beweise erhalten, ohne «detaillierte Kenntnis der Beweisschritte und sogar ohne Kenntnis der letzten Gründe».
Utopisches Projekt
Ein solches utopisches Projekt erregt den tiefsitzenden Widerwillen vieler Mathematiker. Es hat etwas Ehrenrühriges, wenn «dumme» maschinelle Prozeduren die hehre Kunst des Beweises übernehmen. Mathematiker von altem Schrot und Korn sehen im Computer kein Hilfsmittel, sondern einen Störefried, wenn nicht gar einen Usurpator. Aber die Kooperation von Mathematiker und Computer knackt ganz harte mathematische Nüsse. Ein spektakuläres Beispiel ist der sogenannte Vierfarbensatz. Er lautet, grob formuliert: Vier Farben genügen, um eine beliebige Landkarte so zu kolorieren, dass keine aneinander grenzenden Länder die gleiche Farbe haben.
Zu dieser Vermutung aus der Mitte des 19. Jahrhunderts gelang Kenneth Appel und Wolfgang Haken 1976 ein semicomputerisierter Beweis. Der Trick dabei: Ein mathematischer Satz ist oft ein Allsatz, er sagt etwas über alle denkbaren Fälle – hier also Karten – aus. Appel und Haken bewiesen zuerst, dass man das Problem auf etwa 2000 Karten reduzieren kann. Dann liessen sie ein Testprogramm auf diese endliche Zahl von Karten los und bestätigten die Behauptung fallweise. Vielen Mathematikern erschien dies als unelegant und keineswegs stringent: als rohe Gewalt. Mit der unaufhaltsam wachsenden Potenz der Computer verliert dieser Einwand jedoch immer mehr an Gewicht, und nicht wenige Mathematiker sehen es nur als eine Frage der Zeit, bis die Computer in der Kooperation zwischen Mensch und Maschine das Kommando übernehmen werden.
Korrekt oder nicht korrekt
Erwächst also eine Konkurrenz von Supermathematikern aus Silizium? Die Vision ist verführerisch: Man gibt der Maschine einen Beweis ein, lässt sie eine akzeptable Zeit laufen, und sie spuckt schliesslich eine Antwort aus: «Korrekt» oder «Nicht korrekt». Maschinenträumer mögen darob wie einst Pythagoras in Verzückung geraten. Die Probleme sind allerdings unübersehbar. Eines ist die Frage nach einer neuen fundamentalen Sprache. Der russische Mathematiker Vladimir Voevodsky zum Beispiel trägt sich mit dem ambitiösen Projekt einer «univalenten Begründung der Mathematik», einer auf der logischen Typentheorie basierenden neuen Grammatik, die, so seine Meinung, einer computergerechteren Formulierung mathematischer Aussagen zudienen würde. Das ist ein der mengentheoretischen Revolution im 20. Jahrhundert ebenbürtiges konzeptuelles Ereignis.
Einstweilen stellen sich handfestere Probleme, etwa das Dilemma des Überprüfens. Nehmen wir an, ein Beweis sei zu komplex, als dass er von einem Menschen überprüft werden kann; aber delegiert man die Aufgabe an die Maschine, dann erweisen sich deren Schritte womöglich als zu komplex, als dass sie der Mensch nachvollziehen kann. Man schafft sich also mit der Algorithmisierung des Beweises eine technische Extradimension der Fehlbarkeit; eine zudem, die in dem Masse kritischer wird, in dem die Komplexität der automatischen Schritte die Nachvollziehbarkeit durch den Menschen übersteigt. Pierre Deligne, ein Spezialist für algebraische Geometrie und Mathematiker der «alten Schule», formuliert dies so: «Ich bin auf gewisse Weise egozentrisch. Ich glaube einem Beweis, wenn ich ihn verstehe, wenn er klar ist. Menschen machen Fehler, gewiss, aber das tun auch Computer. Nur sind sie bei ihm schwieriger zu entdecken.»
Mathematik als Spiel
Statt «egozentrisch» könnte man auch «anthropozentrisch» sagen. Und damit gibt sich die Frage nach dem Supermathematiker als Strang einer allgemeineren Entwicklung zu erkennen: der Superintelligenz. Maschinen sind zweifellos dem Menschen noch in vielerlei Hinsicht unterlegen, dennoch haben sie bereits in zahlreichen Spielen wie Dame, Backgammon, Schach oder Jeopardy übermenschliches Niveau erreicht. Man kann sich fragen, ob Mathematik nicht auch ein grandioses Spiel sei, dessen Regeln wir einfach nicht kennen oder die zu kennen jenseits des menschlichen Horizonts liegen.
Die Frage stellt sich also, ob denn mathematisches Denken vollständig durch Algorithmen abgedeckt werden könne; oder ob hier nicht noch ein ganz anderes Vermögen hineinspiele: Phantasie, Intuition, heuristisches Gespür, Improvisationsvermögen. Anders gesagt: Mathematisches Denken ist nicht nur mathematisches Denken. Der Informatiker Donald Knuth brachte dies einmal so auf den Punkt: «Die künstliche Intelligenz kann mittlerweile so ziemlich alles, was ‹Denken› erfordert, aber kaum etwas von dem, was Menschen (. . .) gedankenlos tun – das ist irgendwie viel schwieriger!»
Es ist zu früh, Prognosen zu stellen. Aber wenn Computer sich in der Mathematik als immer unentbehrlicher herausstellen, werden wir wohl auch das alte platonische Ideal der absoluten mathematischen Wahrheit einer Revision unterziehen müssen. Die Mathematiker kämen dann nicht darum herum, einzusehen, dass nicht alle ihre Sätze mit dem Siegel des «quod erat demonstrandum» versehen werden können.
Nota. - Das Problem der Nichtüberprüfbarkeit computergenerierter Mathematik wird sich schlechterdings nicht lösen lassen. Es ist aber bloß ein praktisches Problem. Nämlich, an jeweils welcher Stelle je wieviel Unsicherheit in Kauf genommen wird.
Es gibt Bereiche - etwa bei der Kernenergie -, wo keine Unsicherheit tolerierbar ist? Keine Unsicherheiten gibt es in der Wirklichkeit gar nicht, und eine Kernenergie hätte es dann nie geben dürfen. Das ist aber kein mathematisches Problem, sondern eins der Anwendung der Mathematik. Mathematisch ist dagegen die Frage, ob sie noch wahr sein kann, wenn sie nicht überprüfbar ist.
Ist also das wahr, was bereits überprüft wurde? "Was ist Wahrheit!" ruft Pontius Pilatus. Wahr ist, was ohne Bedingungen gilt. Für die Mathematik hieße das bloß: dass ihre Operationen sich allezeit wiederholen lassen. Mit ihrer Anwendbarkeit 'im Leben' hat das gar nichts zu tun: Da treten von außen Bedingungen hinzu, für die die Mathematik nicht verantwortlich ist.
Die Anwendbarkeit von Sätzen kann nur über die Richtigkeit der Sätze etwas aussagen, nicht aber über ihre Wahrheit. Sie könnten wahr sein, auch wenn sich gar nichts damit anfangen lässt. Das wäre dann eine ästhetische Qualität, die sich lediglich anschauen ließe; ich hatte einen Mathematiklehrer, der von der Schönheit seiner Beweise hingerissen war und uns immer wieder einen andern, neuen vorführen musste. Doch wird den meisten Menschen die Mathematik zu schwer vorkommen, um sich nur an ihrem Anblick zu freuen.
Bei philosophischen Wahrheiten gibt es immerhin die Chance, dass sie die eigene Haltung beeinflussen.
JE
