»Zu einem unbestimmten zukünftigen Zeitpunkt werden Mathematiker durch Computer ersetzt.« Die gewagte Vorhersage soll der renommierte Mathematiker Paul Cohen (1934–2007) Berichten zufolge in den 1970er Jahren gemacht haben. Bis heute stößt die Äußerung bei seinen Kollegen auf Gegenwind. Cohen war schon immer ein Querdenker: Seine revolutionären Methoden in der Mengenlehre brachten ihm die Fields-Medaille ein, damit ist er die erste und bisher einzige Person, welche die begehrte Auszeichnung für Arbeiten in der Logik erhalten hat. Zudem vertrat er die kontroverse Meinung, die gesamte Mathematik ließe sich automatisieren, einschließlich des Führens von Beweisen.

Anders als man durch die Erfahrungen aus dem Mathematikunterricht vielleicht denken mag, besteht die Arbeit eines Mathematikers nicht darin, zu rechnen. Seine Hauptaufgabe ist es, formale Aussagen unwiderruflich zu belegen. Ein Beweis ist ein schrittweise geführtes logisches Argument, das überprüft, ob eine Vermutung wahr ist. Sobald sie bewiesen ist, wird eine Vermutung zu einem Theorem (auch Satz genannt). Darüber hinaus erklären Beweise, warum eine Aussage gültig – oder falsch – ist. Gleichwohl sind sie schwer zu fassen, denn die Argumente bewegen sich in einer extrem abstrakten Welt, die nichts mit unseren alltäglichen Erfahrungen zu tun haben. »Wir Menschen sind für die Art von Aufgabe nicht geeignet«, sagt der Kognitionswissenschaftler Simon DeDeo von der Carnegie Mellon University in Pittsburgh.

Bisher setzt man Computer meist ein, um große Berechnungen durchzuführen. Aber Mathematik erfordert etwas anderes. Vermutungen entstehen durch induktives Denken, eine Person muss sich intuitiv über ein interessantes Problem Gedanken machen. Beweise folgen meist einer deduktiven, schrittweisen Logik. Dazu verbindet man häufig komplizierte Zusammenhänge auf kreative Weise und füllt mühsam anschließend alle vorhandenen Argumentationslücken. Maschinen können solche Aufgaben bisher noch nicht meistern.

Dennoch gibt erste Ansätze, wie Algorithmen die Arbeit von Mathematikern unterstützen können. Sie lassen sich in zwei Kategorien unterteilen: Automatisierte Theorembeweiser (englisch: automated theorem proving, kurz: ATP) verwenden in der Regel Brute-Force-Methoden, um große Berechnungen zu tätigen, etwa wenn man zahlreiche Fallunterscheidungen abarbeiten möchte. Interaktive Theorembeweiser (interactive theorem proving, ITP) nehmen dagegen die Rolle eines Assistenten an, der prüft, ob ein logisches Argument richtig ist. Damit kann man mit solchen Algorithmen nach Fehlern in bestehenden Beweisen suchen. Weder ATPs noch ITPs sind allerdings in der Lage, eine logische Argumentationskette zu erzeugen – nicht einmal neuere Theorembeweiser, die beide Ansätze miteinander verbinden. Darüber hinaus stoßen die Programme bei vielen Wissenschaftlern auf Ablehnung. »Sie sind sehr umstritten«, sagt DeDeo. »Den meisten Mathematikern gefällt die Idee nicht.«

Zunächst stellt sich die Frage, inwieweit sich die Beweisführung überhaupt automatisieren lässt: Kann ein Computer eine interessante Vermutung hervorbringen und diese dann auf nachvollziehbare Art belegen? Forschungseinrichtungen auf der ganzen Welt haben in den letzten Jahren die Fortschritte im Bereich der künstlichen Intelligenz genutzt, um der Frage nachzugehen. Josef Urban vom tschechischen Institut für Informatik, Robotik und Kybernetik in Prag nutzt beispielsweise unterschiedliche Ansätze des maschinellen Lernens, um bestehende Beweisprüfer leistungsfähiger zu machen. Im Juli 2020 gelang es ihm und seinen Kollegen, mehrere Vermutungen und Beweise von Computern generieren und überprüfen zu lassen. Bloß einen Monat früher hatten Forscher von Google Research unter der Leitung von Christian Szegedy ihre jüngsten Ergebnisse veröffentlicht, in denen sie natürliche Sprachverarbeitung nutzten, um die von Computern geführten Beweise verständlicher zu machen.

Einige Experten sehen Theorembeweiser als potenziellen Wendepunkt in der Mathematik. Andere entgegnen, Computer seien wahrscheinlich niemals in der Lage, selbstständig stichhaltige Argumentationsketten zu erstellen. Mathematiker, Logiker und Philosophen streiten schon lange darüber, welche Schritte beim Führen eines Beweises menschliche Fähigkeiten benötigen. Die Debatten dauern bis heute an, insbesondere in den Forschungsbereichen, welche die reine Mathematik mit der Informatik verbinden.

Für Informatiker dagegen sind Theorembeweiser keineswegs umstritten. Sie verfolgen das ehrgeizige Ziel der automatisierten Beweisführung weiter, denn es könnte auch ihr Fachgebiet maßgeblich beeinflussen. Wäre ein System in der Lage, eine bisher unbekannte Vermutung vorherzusagen oder ein neues Theorem zu belegen, hätte man einen neuen Meilenstein erreicht: eine maschinelle Version des Verstehens, so Szegedy. Damit ließe sich vielleicht irgendwann die menschliche Vernunft automatisieren.

KI entwickelt effiziente Verschlüsselung

Darüber hinaus können bereits existierende Theorembeweiser überprüfen, ob ein Programm funktioniert. Die philosophischen Bedenken, ob eine Maschine so intuitiv und kreativ wie ein Mensch handeln kann, spielen für Computerwissenschaftler eine eher untergeordnete Rolle. Stattdessen konzentrieren sie sich darauf, einen effizienten Weg zum Lösen mathematischer Probleme zu finden. Am Massachusetts Institute of Technology hat zum Beispiel der Informatiker Adam Chlipala einen Theorembeweiser entworfen, der kryptografische Algorithmen erzeugt, um digitale Transaktionen zu sichern. Solche Programme haben bisher sonst immer Menschen geschrieben. Inzwischen nutzt der Google-Browser Chrome den computergenerierten Code für den Großteil der darüber stattfindenden Kommunikation.

In der Mathematik haben Algorithmen dazu beigetragen, komplizierte und insbesondere zeitaufwändige Beweise auszuarbeiten, die sonst hunderte Jahre in Anspruch genommen hätten. Die keplersche Vermutung, bei der es um die dichteste Anordnung von Kugeln geht, bietet ein aufschlussreiches Beispiel dafür. Im Jahr 1998 fand Thomas Hales zusammen mit seinem Studenten Sam Ferguson einen Beweis für die Lösung des Problems – doch die Hauptarbeit erledigte ein Computer: Die Maschine spielte zahlreiche verschiedene Fälle durch, wie man die Kugeln stapeln könnte, und schloss so eine Möglichkeit nach der anderen aus. Das Ergebnis war extrem umfangreich (es nahm 3 Gigabyte Speicherplatz in Anspruch), weshalb zwölf Mathematiker es jahrelang untersuchten, bevor sie verkündeten, es sei mit 99-prozentiger Sicherheit richtig.

Die keplersche Vermutung ist nicht die einzige berühmte Frage, die Computer beantwortet haben. Der Vier-Farben-Satz, dem zufolge man nur vier verschiedene Farben braucht, um eine zweidimensionale Landkarte zu bemalen, ohne dass zwei angrenzende Regionen gleich gefärbt sind, lösten Heinrich Heesch, Kenneth Appel und Wolfgang Haken bereits 1976 mit Hilfe eines Computerprogramms. Dabei durchwühlte der Algorithmus alle möglichen Varianten von Karten mit fünf Farben und zeigte, wie sich jede von ihnen auf vier Farben reduzieren lässt.

Zudem verwendeten drei Mathematiker 2016 ein Computerprogramm, um das Problem der booleschen pythagoräischen Tripel zu beweisen. Dabei geht es um die Frage, ob es möglich ist, alle natürlichen Zahlen rot und blau einzufärben, wobei kein pythagoräisches Tripel (also alle Zahlen a, b und c mit a² + b² = c²) aus rein roten oder blauen Gliedern bestehen darf. Wie die Forscher zeigten, ist das bloß bis zu der Zahl 7824 realisierbar. Die Lösung war extrem rechenintensiv, sie nahm in ihrer ersten Version über 200 Terabyte in Anspruch. Selbst mit einer Hochgeschwindigkeits-Internetverbindung dauerte es etwas mehr als drei Wochen, um das Ergebnis herunterzuladen.

Einige Wissenschaftler preisen die genannten Beispiele als Erfolge, doch die computergenerierten Beweise fachen die Debatte weiter an. Zum Beispiel ist der über 40 Jahre alte Algorithmus zum Nachweis des Vier-Farben-Satzes so umfangreich, dass ein Mensch ihn unmöglich allein überprüfen kann. »Seitdem streiten sich Experten, ob es sich dabei tatsächlich um einen Beweis handelt oder nicht«, sagt der Mathematiker und Blogger Michael Harris von der Columbia University.

Zudem führen die Algorithmen zu weiteren Schwierigkeiten. Möchte man einen Theorembeweiser verwenden, muss man dafür nicht nur programmieren können, sondern auch herausfinden, wie man ein mathematisches Problem in computerfreundlicher Sprache ausdrückt. Das ganze Unterfangen ist sehr zeitaufwändig und lenkt von der eigentlichen Arbeit eines Forschers ab. »Bis ich meine Frage in eine passende Form gebracht habe, könnte ich das Problem einfach selbst lösen«, sagt Harris.

Viele Wissenschaftler sehen keinen Bedarf an Theoremlösern. »Wir haben bereits ein funktionierendes System: Es besteht aus Bleistift und Papier«, sagt Kevin Buzzard vom Imperial College London, der vor drei Jahren seine Arbeit von der reinen Mathematik auf computergestützte Theorembeweiser umstellte. »Computer haben für uns erstaunliche Berechnungen durchgeführt, aber sie haben noch nie ein schwieriges Problem ganz allein gelöst«, sagt er. »Solange sie das nicht tun, werden sich Mathematiker nicht darauf einlassen.«

Buzzard und einige seiner Kollegen finden trotzdem, man sollte den neuen Methoden eine Chance geben. Tatsächlich sind von Computern geführte Beweise vielleicht gar nicht so schwer nachzuvollziehen, wie viele annehmen, erklärt DeDeo. Kürzlich hat er zusammen mit Scott Viteri, einem Informatiker, der jetzt an der Stanford University forscht, mehrere berühmte klassische Beweise (darunter einen aus Euklids »Elementen«) mit dutzenden neuen Beweisen, die ein Algorithmus namens »Coq« erarbeitet hat, verglichen, um nach Gemeinsamkeiten zu suchen. Wie sie herausfanden, ähnelt die vernetzte Struktur der maschinengenerierten Ergebnisse den menschlichen Werken. Das könnte Forschern helfen, den Algorithmen beizubringen, ihr Vorgehen zu erklären.

Ein nützliches Lehrmittel, um Probleme strukturiert anzugehen

Andere Wissenschaftler sehen in Theorembeweisern nützliche Lehrmittel, die sich sowohl in der Informatik als auch in der Mathematik bezahlt machen könnten. An der Johns Hopkins University hat die Mathematikerin Emily Riehl beispielsweise Kurse konzipiert, in denen Studenten formale Aussagen mit einem Computer belegen. »Das zwingt sie, sehr organisiert zu sein und klar zu denken«, sagt sie. »Studenten, die zum ersten Mal einen Beweis führen, tun sich schwer damit, zu wissen, was sie brauchen, und die zu Grunde liegende logische Struktur zu erkennen.«

In ihrer eigenen Forschungsarbeit verwendet Riehl ebenfalls zunehmend Theorembeweiser. »Das ist nicht unbedingt etwas, was man ständig nutzen muss. Es wird niemals das Herumkritzeln auf einem Blatt Papier ersetzen«, sagt sie, »aber die Verwendung von Computerprogrammen hat meine Einstellung zum Schreiben von Beweisen verändert.«

Die Theoremlöser bieten darüber hinaus eine Möglichkeit, bekannte Arbeiten auf Fehler hin zu prüfen. 1999 entdeckte der russisch-amerikanische Algebraiker Vladimir Voevodsky mit einem solchen Programm beispielsweise eine Ungenauigkeit in einem seiner Beweise. Ab dem Zeitpunkt bis zu seinem Tod 2017 war Voevodsky daher ein lautstarker Befürworter von computergestützten Beweisassistenten. Hales sagt, er und Ferguson hätten Hunderte von Fehlern in ihrer Arbeit gefunden, als sie diese mit einem Computer überprüften. Selbst der erste Satz in Euklids »Elementen« ist nicht perfekt.

Wenn eine Maschine Mathematikern helfen kann, solche Fehler zu vermeiden, warum sollte man sie dann nicht nutzen? Ein häufig genannter Einwand – ob gerechtfertigt oder nicht – ist laut Harris: Wenn Wissenschaftler ihre Zeit damit verbringen, Mathematik zu formalisieren, damit ein Computer sie versteht, geht das von der Zeit ab, die sie mit neuer Forschung verbringen könnten.

»Bis ich mein Problem passend formuliert habe, kann ich es auch selbst lösen«Michael Harris, Mathematiker

Der Fields-Medaillen-Gewinner Timothy Gowers von der University of Cambridge ermuntert seine Kollegen dagegen, noch weiter zu gehen: Er träumt von einer Zukunft, in der Theorembeweiser menschliche Gutachter bei großen Fachzeitschriften ersetzen. »Ich kann mir vorstellen, dass es zum Standardverfahren wird, eine eingereichte Arbeit erst durch einen automatisierten Prüfer zu führen«, sagt er. Doch bevor Computer so weit sind, müssen Forscher eine bedeutende Hürde überwinden: die Kommunikationsbarriere zwischen Mensch und Maschine.

Heutige Algorithmen sind nicht mathematikerfreundlich konzipiert. Zwar kann man mit automatisierten Theorembeweisern (ATPs) aufwändige Fallunterscheidungen durchlaufen, wie im Beispiel der keplerschen Vermutung. Dazu programmiert man alle Regeln ein, die für das zu lösende Problem relevant sind, und fragt anschließend, ob eine bestimmte Vermutung den auferlegten Regeln folgt. Der Computer erledigt dann die gesamte Arbeit.

Aber hier liegt der Hund begraben: Ein ATP erklärt seine Arbeit nicht. Alle Berechnungen finden innerhalb der Maschine statt. Das menschliche Auge nimmt nur eine lange Kette von Nullen und Einsen wahr. Der Computerwissenschaftler Daniel Huang, der die University of California in Berkeley kürzlich für ein Start-up verlassen hat, sagt, es sei unmöglich, eine solche Argumentation nachzuvollziehen, weil sie wie ein Haufen zufälliger Daten aussieht. »Kein Mensch wird sich jemals derartige Beweise ansehen und sagen können: ›Ich hab’s verstanden‹«, betont er.

Interaktive Theorembeweiser (ITPs) funktionieren anders. Sie verfügen über riesige Datensätze mit bis zu Zehntausenden von Theoremen und Beweisen, auf die sie zurückgreifen, um zu überprüfen, ob ein Argument korrekt ist. Im Gegensatz zu ATPs, die wie eine Black Box arbeiten und bloß eine Antwort ausspucken, benötigen ITPs menschliche Führung. »Damit lässt sich nachvollziehen, auf welchen Elementen ein generierter Beweis basiert«, sagt Huang.

ITPs sind in den letzten Jahren immer beliebter geworden. 2017 verwendeten die drei Mathematiker, die das Problem der booleschen pythagoräischen Tripel gelöst haben, ein solches Programm namens »Coq«, um ihre Arbeit zu verifizieren. Darüber hinaus griff Georges Gonthier von Microsoft Research Cambridge im Jahr 2005 auf »Coq« zurück, um den Vier-Farben-Satz zu formalisieren. Für den Beweis der keplerschen Vermutung nutzte Hales gleich zwei ITPs namens »HOL Light« und »Isabelle«.

Die größte Herausforderung auf dem Gebiet der automatisierten Beweisführung ist, Computern logisches Schlussfolgern beizubringen. Informatiker kombinieren dazu ATPs mit ITPs und integrieren zudem Methoden des maschinellen Lernens, um die Theorembeweiser effizienter zu gestalten. Sie hoffen, künftig Programme entwerfen zu können, die ähnlich wie ein Mensch deduktive Schlüsse ziehen und damit mathematische Ideen entwickeln können.

Sprache zuerst, dann die Mathematik

Um logisches Denken zu automatisieren, muss man Szegedy zufolge aber erst herausfinden, wie man erfolgreich natürliche Sprache computergestützt verarbeitet. Die Aufgabe ist inzwischen ein wichtiger Forschungsbereich in der Informatik. Wenn es Algorithmen gelingt, Muster beim Verwenden von Wörtern und Sätzen zu erkennen, dann könnte man ihnen genauso beibringen, nützliche Beweise zu finden – und vor allem sie zu erklären. In den letzten Jahren haben Wissenschaftler in diesem Zusammenhang unter anderem neuronale Netze untersucht, also Algorithmen, die an die Funktionsweise des menschlichen Gehirns angelehnt sind.

Inspiriert von der schnellen Entwicklung KI-gestützter Programme wie AlphaZero (dem Algorithmus von DeepMind, das Menschen beim Schach, Go und Shogi besiegte), wollen Szegedy und sein Team die jüngsten Fortschritte der Spracherkennung nutzen, um formale Beweise zu führen. Anhand vorausgehender Trainingsdaten sagen so genannte Sprachmodelle Zeichenfolgen vorher, die auf eine bestimmte Eingabe folgen könnten. Damit sind die Programme in der Lage, sinnvolle Texte oder Formeln zu generieren.

Szegedys Gruppe bei Google Research hat im Juni 2020 eine Möglichkeit vorgestellt, Sprachmodelle zu verwenden, um mathematische Inhalte zu generieren. Nachdem sie ihr Programm darauf trainiert hatte, eine baumartige Struktur in bereits etablierten Theoremen zu erkennen, ließ sie das Netzwerk ohne weitere Anleitung neue Sätze erzeugen und beweisen. Von den tausenden gefundenen Vermutungen waren etwa 13 Prozent sowohl beweisbar als auch neu (das heißt, sie duplizierten keine anderen Theoreme in der Datenbank). Damit könnten sich Algorithmen tatsächlich selbst beibringen, wie man korrekt Beweise führt. »Neuronale Netze sind in der Lage, eine künstliche Art der Intuition zu entwickeln«, davon ist Szegedy überzeugt.

Josef Urban verfolgt ebenfalls einen Ansatz, bei dem er ITPs, ATPs und künstliche Intelligenz miteinander verbindet. Im Juli 2020 trainierte er mit seiner Forschungsgruppe ein neuronales Netz mit Beispieldaten von mathematischen Beweisen, woraufhin es zahlreiche neue Vermutungen lieferte. Inspiriert hatte Urban die Arbeit des Informatikers Andrej Karpathy, der vor einigen Jahren ein neuronales Netz entwickelt hatte, das mathematisch anmutenden Unsinn erzeugte. Anders als Karpathy wollte Urban aber sinnvollen Inhalt generieren. Deshalb entwarf er mit seiner Gruppe ein eigenes Netzwerk, das unter anderem das Sprachmodell GPT-2 von OpenAI verwendet. Urban und sein Team fütterten ihren Algorithmus mit etlichen Theoremen und dazugehörigen Beweisen und ließen ihn anschließend nach neuen Vermutungen suchen, deren Gültigkeit sie mit einer ATP namens »E« überprüften.

Tatsächlich schlug das Netzwerk mehr als 50 000 Formeln vor, allerdings handelt es sich bei den meisten davon um Duplikate bereits bekannter Gleichungen. »Offenbar sind wir noch nicht in der Lage, wirklich interessante Zusammenhänge zu finden«, sagt Urban.

Trotz all der beeindruckenden Fortschritte ist noch unklar, ob sich die Prophezeiung Cohens von vor über 40 Jahren erfüllen wird. Auch Gowers ist überzeugt davon, Computer würden bis 2099 in der Lage sein, Mathematiker zu übertreffen. Harris ist da anderer Meinung. Er bezweifelt sogar, dass Theorembeweiser überhaupt nützlich sind. Falls Informatiker jemals eine Art synthetische Intuition schaffen sollten, so Harris, dann wird sie nicht mit der des Menschen konkurrieren können. »Selbst wenn Computer anfangen, Dinge zu verstehen, werden sie das niemals auf menschliche Art und Weise tun.«