Computer können Rechnungen viel schneller und zuverlässiger ausführen als jeder Mensch – daran haben wir uns längst gewöhnt. Aber wie ist das mit Aufgaben, für die man mathematische Kreativität braucht? Können Computer auch hilfreich sein, wenn es um das Auffinden von Theoremen, das Beweisen von Aussagen, das Überprüfen mathematischer Argumentationen geht?
Ja, das können sie, sagt Stefan Hetzl vom Institut für Diskrete Mathematik und Geometrie. Er organisierte am 18. und 19. September an der TU Wien ein Symposium, in dem mehrere Vortragende in die Grundkonzepte von „Lean“ einführten – einem Softwaretool, das in den letzten Jahren für Aufsehen sorgte und das Potenzial hat, den Alltag in der Forschung ähnlich zu revolutionieren wie einst Computer oder Taschenrechner.
Was heißt hier „bewiesen“?
Peter Scholze, ein Fields-Medaillen-Gewinner, gilt als einer der berühmtesten Mathematiker unserer Zeit. Im Jahr 2019 quälte er sich mit einem besonders schwierigen Beweis aus dem Gebiet der „verdichteten Mathematik“. Das Argument war kompliziert, Scholze musste viele Konzepte und Aussagen gleichzeitig im Kopf behalten, immense Konzentration war dafür notwendig. Nach anstrengenden Tagen schien der Beweis fertig – doch war er wirklich richtig? Konnte man sich auf ihn verlassen?
Oft ist es in solchen Fällen schwierig, jemanden zu finden, der einen solchen Beweis wirklich exakt nachvollziehen und überprüfen kann. Und selbst wenn es gelingt, vergeht viel Zeit, bis man ein Ergebnis bekommt. Wäre es nicht großartig, wenn man Computer als Assistenten verwenden könnte? Wenn man eine logisch präzise, maschinenlesbare Sprache hätte, in der man Beweise formulieren und ihre Korrektheit garantieren kann?
Der Computer als Beweis-Assistent
Genau das ist heute möglich: Man kann Beweisassistenten-Software entwickeln, die es schafft, die logische Struktur von Beweisen zu erfassen und zu überprüfen. Mit herkömmlicher künstlicher Intelligenz, wie man sie etwa von ChatGPT kennt, hat das allerdings wenig zu tun, erklärt Stefan Hetzl: „Mit AI meint man heute meistens statistische Ansätze, die mit großen Datenmengen trainiert wurden. Diese Methode ist zwar sehr vielseitig, liefert aber Ergebnisse, die nicht erklärt werden und manchmal einfach falsch sind. Für mathematische Beweisführung reicht das alleine nicht aus."
In der Mathematik setzt man daher auf technisch völlig andere Ansätze, die eher mit einer Programmiersprache vergleichbar sind als mit der natürlichen Sprache, in der man mit ChatGPT kommuniziert. Der Computer schafft es dadurch, bestehende mathematische Arbeiten aus Büchern oder Artikeln zu verarbeiten. Dadurch können neue Beweise oder Aussagen logisch mit dem bestehenden Wissen der Mathematik verknüpft werden. Der Computer kann nachrechnen, ob eine neue Aussage tatsächlich aus bereits bestehendem Wissen folgt oder nicht.
Erste Schritte: Das Vier-Farb-Problem
Dass man mit Computern nach mathematischen Beweisen sucht, ist nicht neu. Berühmt wurde die Geschichte vom Vier-Farben-Satz: Wenn man die Länder auf einer gewöhnlichen, zweidimensionalen Landkarte einfärben möchte, sodass niemals zwei benachbarte Länder dieselbe Farbe zugewiesen wurde – wie viele verschiedene Farben sind dafür mindestens nötig? Der Vier-Farben-Satz, der bereits 1852 als Vermutung formuliert wurde, sagt: Vier Farben reichen dafür aus. Man kann das leicht an verschiedenen Landkarten testen, doch ein Beweis, dass es mit jeder beliebigen Landkarte möglich sein muss, blieb lange aus.
Die Zahl denkbarer Landkarten ist unendlich groß. Allerdings konnte man zeigen, dass es genügt, eine bestimmte Liste problematischer Fälle durchzugehen, um den Vier-Farben-Satz allgemein beweisen zu können. Knapp 2000 Fälle waren es, die durchprobiert werden mussten – und dafür verwendete man einen Computer. Der kam im Jahr 1976 zu dem Schluss: Es klappt tatsächlich immer, der Vier-Farben-Satz ist korrekt.
Es war der erste mathematische Beweis, der mit Hilfe eines Computerprogramms geführt wurde. „Doch das, worum es uns heute geht, ist etwas völlig anderes“, erklärt Stefan Hetzl. „Beim Vier-Farben-Satz ging es einfach nur um mechanisches Durchprobieren einer großen Zahl von Möglichkeiten. Heutige Beweis-Assistenten hingegen bilden die logische Struktur von Beweisen ab, man könnte sagen: In gewissem Sinn verstehen sie die Beweise.“
Lean – die Software, die den Durchbruch bringt?
Immer klarer wurde nun in den letzten Jahren, wie weit diese Beweis-Assistenten bereits fortgeschritten sind. Für großes Aufsehen in der mathematischen Community sorgte die Beweis-Assistenz-Software Lean. Sie wurde eingesetzt, um den hochkomplexen Beweis von Peter Scholze zu untersuchen. Scholze arbeitete mit einem Team zusammen, das schon seit Jahren an Lean forschte, und tatsächlich gelang es, seinen Beweis auf passende Weise zu formalisieren. Bald stellte sich heraus: Der Beweis war korrekt.
Für die Welt der Mathematik war das eine Sensation: Erstmals wurde ein Beweis-Assistent eingesetzt, um einen wichtigen mathematischen Beweis mit weitreichenden Konsequenzen für die Forschung zu erstellen. „Lean liefert nicht nur die wasserdichte Verifikation, dass ein Beweis stimmt“, sagt Stefan Hetzl. „Oft werden im Zuge der Arbeit mit einem solchen Beweis-Assistenten Theorien und Beweise verbessert, Formulierungen angepasst oder kleine Fehler korrigiert".
Langfristig, so ist Hetzl überzeugt, eröffnen sich dadurch ganz neue Perspektiven für die Mathematik: Bei der Suche nach mathematischen Sätzen oder beim Durchführen kleinerer Umbauarbeiten an bestehenden Theorien könnte der Computer zum Einsatz kommen. „Auch die Zusammenarbeit zwischen Menschen in der Mathematik kann dadurch dramatisch verbessert werden“, glaubt Stefan Hetzl. „Durch den Beweis-Assistenten wird Parallelisierung möglich. Vielleicht lässt sich ein schwieriges Problem in Dutzende Teilprobleme zerlegen, an denen dann unterschiedliche Menschen arbeiten. Aber der Beweis-Assistent stellt sicher, dass am Ende alles korrekt und konsistent zusammengefügt wird.“
Die Mathematik könnte also vor einem fundamentalen Kulturwandel stehen: Es geht nicht darum, dass menschliche Arbeit durch den Computer ersetzt wird – der Computer könnte in der Zusammenarbeit mit Menschen neue Möglichkeiten eröffnen, die sonst niemals erreicht worden wären.
Rückfragehinweis
Prof. Stefan Hetzl
Institut für Diskrete Mathematik und Geometrie
Technische Universität Wien
+43 1 58801 10421
stefan.hetzl@tuwien.ac.at