Der mathematische Beweis im Zeitalter der Algorithmen 

Was, wenn Mathematiker den Computer nicht mehr verstehen?

Was ist ein Beweis? Das ist das tiefste erkenntnistheoretische Problem der Mathematik. Der Beweis garantiert die Geltung mathematischer Sätze. Und in ihnen sieht man die höchste Art der Wahrheit. Unumstösslich, ewig, weil sie Sachverhalte beschreiben, die «nicht von dieser Welt» sind: platonisch. Der Satz von Pythagoras ist ein solcher Sachverhalt. Er existiert in einem Reich, über dessen Seinsweise die philosophierenden Mathematiker allerdings nie eins wurden. 

***

Aus diesem Grund wuchs um die Wende vom 19. zum 20. Jahrhundert das Bedürfnis, das Fundament der Mathematik philosophisch zu «reinigen», indem man ihr eine logisch makellose Architektur zugrundelegt. Das ist die grandiose Idee einer Beweismaschine, die kraft einer Formalsprache sowie klarer Schlussregeln aus einer endlichen Anzahl von Axiomen alle mathemati-schen Sätze deduziert. Nach dem Konsens der Mathematiker geht die Mengenlehre - das Fundament der Mathematik - von 10 Standardannahmen aus, den sogenannten Zermelo-Fraenkel-Axiomen. Tatsächlich gibt es zahlreiche Sätze, deren Wahrheit man vermutet, deren Beweis aber aussteht. Eine Beweismaschine wäre ein Geschenk des platonischen Himmels. Man müsste ihr einfach ein Theorem vorlegen, und innert endlicher Frist würde sie das Theorem aus den Axiomen deduzieren. 

Ein Wunschtraum, den der Logiker Kurt Gödel in den 1930er Jahren zerstörte. Er zeigte, dass nur schon eine Maschine, in der sich die Arithmetik formalisieren lässt, nicht alle arithmetischen Sätze aus den zugrundegelegten Axiomen beweisen kann. Das System lässt sich erweitern, aber es bleibt in diesem Dilemma gefangen. Der britische Mathematiker Alan Turing doppelte in den 1950er Jahren nach, als er zeigte, dass es Sätze gibt, bei denen die Beweismaschine keine Antwort liefert, das heisst in unendlichen Leerlauf gerät. Wenn also schon die Arithmetik in diesem Sinn unvollständig ist, wie steht es um die ganze Mathematik? Was hat es für einen Sinn, von der Wahrheit eines Theorems zu sprechen, wenn es nicht beweisbar ist? 

***

Die Frage zielt direkt auf die Fundamente der Mathematik. Und sie hat den kanadischen Mathematiker Andrew Granville veranlasst, einen neuen, pragmatischeren Gesichtspunkt in die Debatte einzubringen. Kurz gesagt lautet seine These: Letztlich beruht der Beweis auf einer Übereinkunft unter den Mathematikern. Mathematik ist ein Sprachspiel mit Regeln und Normen, und die Objektivität – die «Wahrheit» - ihrer Sätze ist durch ein solches Sprachspiel be-gründet. Wie Granville schreibt, besteht das beste System in der Mathematik darin, «dass viele Forscher einen Beweis aus verschiedenen Perspektiven prüfen, und dass dieser Beweis gut in einen Kontext passt, den sie kennen und dem sie vertrauen. In einem gewissen Sinn sagen wir nicht, wir wüssten, der Satz sei wahr. Wir sagen, wir hofften, er sei korrekt, weil eine Vielzahl von Leuten ihn aus verschiedenen Blickwinkeln gestestet haben». So gibt es zum Beispiel über 400 Beweise des Satzes von Pythagoras.  Deshalb wäre es wahrscheinlich unverfänglicher, statt von der Wahrheit von Theoremen von ihrer Robustheit zu sprechen. 

***

Eine solche Sichtweise gewinnt nun an unerwarteter Aktualität, wenn wir die neuesten KI-Systeme in die Diskussion einbeziehen. Sie lernen ja immer mehr intellektuelle Fähigkeiten des Menschen, sie lernen auch Mathematik. Im gegenwärtigen Vertrauen in die Gelehrigkeit von Computern stellt sich die Frage, wie es denn um einen künstlichen Mathematiker stünde, um ein KI-System also, das Mathematik von den elementaren arithmetischen Grundlagen auf lernen und die rechnerischen, logischen und metamathematischen Kompetenzen schrittweise selbst erwerben und entwickeln würde, bis es schliesslich die Stufe eines künstlichen Supermathematikers erreicht hätte. Es wäre nicht nur in der Lage, die uns bekannten mathematischen Theoreme zu beweisen, es würde auch bisher ungelöste Probleme bewältigen, auf eine Art und Weise freilich, die den Mathematikern Kopfzerbrechen bereitet. Seine Spielzüge wären  für den Menschen eine Black Box. Was aber ist ein mathematischer Beweis, wenn die Mathematiker ihn nicht verstehen?

***

Die Frage ist brisant, denn sie ist vom fiktiven Szenario ins reale übergetreten. Kürzlich entwickelte Deep Mind von Google zwei KI-Systeme – Alpha Proof und Alpha Geometry 2 -, die komplexe Probleme lösen.  Und schon seit längerem lassen sich Mathematiker von Beweisassistenten helfen. Zum Beispiel von Lean, einem System, das 2013 entwickelt worden ist. Grosse Teile des mathematischen Wissens finden sich darin in eine Computersprache übersetzt. Schlägt man einen Beweis vor und formuliert ihn in Lean, vollzieht ihn das System Schritt für Schritt nach und versieht ihn mit dem Siegel «korrekt» oder «nicht korrekt». 

Aber wie robust ist der Beweis eines Theorems, der von einem KI-System geliefert wird? Bekanntlich können KI-Systeme «halluzinieren». Sie generieren Output, der nur scheinbar mit dem Input zusammenhängt: Fake-Beweise. Ein Bot lieferte zum Beispiel den «Beweis», dass zwischen zwei ganzen Zahlen unendlich viele ganze Zahlen existieren. 

Oder der Fall könnte eintreffen, dass ein Programmierer vergisst, den Trainingsalgorithmus eines neuronalen Netzwerks anzuhalten. So soll es vorgekommen sein, dass ein solcher «vergessener» Algorithmus selbständig eine neue Form der Addition herausgefunden hat (sogenannte modulare Addition), die man ihn nicht lehrte. Im Maschinenlernen nennt man diese neuen Einsichten des Computers «Grokking». Was also, wenn der Computer Beweise «grokkt», die unseren Begriffshorizont übersteigen? 

Hier nimmt eine neue Interaktionsform zwischen Mensch und Maschine Gestalt an, in der der Computer seinen «autonomen» Beitrag zum Wissenskorpus leistet. Die Mathematiker müssten ihm das Vertrauen in die Beweiskompetenz schenken, und das heisst, sie müssten ihn in ihre Community aufnehmen. Anzunehmen ist dabei, dass das Zusammenspiel von menschlichen und künstlichen Mathematikern durchaus den Beweis eines schwierigen Theorems erlaubt. Erneut stellt sich also die Frage der Übereinkunft als Basis des Beweises. Übereinkunft zwischen Mensch und Computer? Und wenn die Computer mit der Zeit die ganze Arbeit übernehmen würden? 

***

Das ist äusserst unwahrscheinlich. Denn gerade die Kooperation mit dem Computer kann möglicherweise den Unterschied zwischen Mensch und Maschine deutlicher hervortreten lassen. Mathematik ist eine geistige Terra incognita. Es zeugt von einem völlig falschen Verständnis für sie, wenn man den Beweis als Abschnurren formallogischer «maschineller» Schritte betrachtet. Er ist im Gegenteil ein hoch kreativer Prozess, der sehr viel an intuitiver Einsicht, Einfallsreichtum, Umgang mit Paradoxien, «unscharfem» Denken voraussetzt. KI-Modelle werden ja auf dem Korpus der niedergeschriebenen mathematischen Arbeiten trainiert. Aber wie die KI-Forscherin Katie Collins von der University of Cambridge bemerkt, sind «online wenig Daten über formalisierte Mathematik zu finden, verglichen mit Daten in natürlicher Sprache». Das ist kaum verwunderlich, denn kreative Mathematiker wissen in der Regel mehr, als sich in Programmsprachen codieren lässt. Und aus diesem Grund ist es fraglich, ob man diesen impliziten Rumpf der Mathematik jemals völlig explizite darstellen kann.  

Das heisst, die Mathematik wird sich im Zeitalter der KI als das zu erkennen geben, was sie schon immer war: als eine Kunst des Vermutens, die in glücklichen Fällen zu robusten Resultaten führt.