Herr Krapp, worum ging es in dem offenen Problem?

Lothar Sebastian Krapp: Das Problem betrifft sogenannte arithmetische Progressionen im mathematischen Gebiet der Diskrepanztheorie. Im Wesentlichen geht es darum, wie sehr spezielle Zahlen verteilt sind. Es geht um die Eigenschaften von bestimmten Zahlenfolgen.

Wie funktioniert ein solcher mathematischer Beweis?

Ein Beweis sind logische Argumentationsschritte. Es ist nicht einfach nur eine Umstellung von Gleichungen, wie man es vielleicht aus der Schule kennt, sondern es geht darum, eine logische Schlussfolgerung zu führen. Man beginnt bei bereits bekannten Prinzipien und versucht in einer logischen Argumentation bei dem anzukommen, was man beweisen möchte. Das erfordert die Kenntnis von vielen kleinen Beweisstrategien und auch die mathematische Intuition, wie sie anzuwenden sind.

Weil der Beweis aus logischen Schritte besteht, die aufeinander folgen und sich ganz gut von einem Computer formalisieren lassen, sind wir hier auf einem Gebiet, das computergestützte Beweise zulässt.

Wie gelang es der KI, den Beweis zu führen?

Der Knackpunkt ist: Um den Beweis zu tätigen, hat man eine moderne generative KI mit einem klassischen algorithmischen Programm zusammengeschaltet, in diesem Fall war es unter anderem der Beweisassistent Lean. Lean ist keine generative KI. Es ist ein klassisches, regelbasiertes Programm, bei dem keine Zufallsmechanismen im Hintergrund laufen. Streng genommen hat also nicht die KI diesen Beweis entwickelt, sondern sie hat das Programm Lean verwendet, um den Beweis computerverifiziert zu erstellen. Anstatt dass der Mensch vor dem Computer sitzt und die Codeeingabe beim Beweisassistenten macht, übernimmt die KI seine Rolle.

Die KI hat also den Beweisassistenten Lean „gefüttert“ und zu einer Folge an Schritten veranlasst, die dann zu diesem Beweis geführt hat? Das klingt ein wenig nach Fleißarbeit.

Es ist Fleißarbeit, aber Fleißarbeit mit Intuition. Es ist nicht nur bloßes Ausprobieren. Man darf nicht denken, dass es brute force ist, mit der alles einfach ausprobiert worden ist, sondern da steckt schon Intuition dahinter. Hier hat man es offensichtlich geschafft, die mathematische Intuition des Zahlentheoretikers durch das Wahrscheinlichkeitsmodell, das im Hintergrund der KI läuft, recht gut wiederzugeben.

KI basiert auf einem stochastischen Prozess. Sie ist eigentlich eine große Zufallsmaschine. Was bedeutet das für den mathematischen Beweis? Schürt dies Bedenken?

Nein, keinerlei Bedenken. Solange ein Beweisassistent zwischengeschaltet ist, der nicht einem stochastischen Prozess folgt, sondern die logische Schlussfolgerung hart überprüft, habe ich keine Zweifel. Diesem Programm vertraue ich uneingeschränkt. Glaubt also die Mathe-Community diesem computergeschriebenen Beweis? Ich habe das Gefühl, dass es da keine Gegenstimmen gibt.

Die Kopplung der KI mit einem Beweisassistenten war eigentlich der nächste logische Schritt. Dass da so schnell etwas herauskommt, das hätte ich aber auch nicht unbedingt erwartet.

Warum kam die KI auf die Lösung, der Mensch jedoch nicht?

Vielleicht ist einfach noch niemand auf die drei richtigen Ideen gestoßen. Oft ist es so, dass Beweise ein paar neue Ideen brauchen, die bisher noch nicht da waren. Und ob man darauf kommt oder nicht, ist auch in der Mathematik in gewisser Weise Zufall. Das ist die mathematische Kreativität. Es ist aber nicht so, dass der Mensch es nicht hinbekommen hätte.

© Universität Konstanz, Inka Reiter

Lothar Sebastian Krapp im Gespräch.

KI ist also prinzipiell eine sinnvolle Unterstützung für die mathematische Community im Bereich der Beweisführung?

Ja. Wenn es darum geht, dass eine offene Frage bewiesen werden soll und wir einfach deren Wahrheitsgehalt bestätigen wollen, dann auf jeden Fall. Vor allem für praktische Resultate finde ich das auch sehr gut. Ich sehe das Einsatzgebiet aber viel mehr in der Informatik – da muss der Programmiercode funktionieren, da muss die Formel stimmen. Und ob eine Formel stimmt, woher wissen wir das? Das wissen wir nicht durch ausprobieren, sondern nur durch einen mathematischen Beweis.

Ist der Beweis durch KI eine mathematische Sensation?

Nein, das für mich keine große Meldung. Es ist jetzt halt einfach zum ersten Mal passiert. Es wird immer wieder passieren, weil wir jetzt mit der KI einen Akteur haben, der relativ gut das machen kann, was der Mensch sonst „von Hand“ tut.

Wir sollten die KI als das betrachten, was sie ist: ein unterstützendes, textschreibendes Programm, das jedoch kleinere logische Schritte selbst führen kann, die für einen gediegenen Mathematiker manchmal auch einfach nur lästig sind.

Wir sind momentan gerade in der besten Zeit dafür – weil wir noch genügend Leute haben, die den Beweis nachprüfen können. Was jedoch eine negative Vorstellung wäre: dass sich Studierende nicht mehr damit auseinandersetzen, wie man einen Beweis schreibt, weil KI dies übernehmen kann. Und dass gleichzeitig das Internet mit KI-generierten Beweistexten überflutet wird. Denn da ist auch viel Schrott mit dabei.

Verschieben sich gerade die Grenzen des Machbaren in der Mathematik?

Die reine Mathematik wird ja oft als Kunst beschrieben. Es geht darum, die menschlichen Grenzen zu testen: Wie abstrakt kann ein Mensch denken, um auf solche Lösungen zu kommen? Es geht darum zu wissen: Wozu ist der Mensch fähig?

In gewisser Weise wurde das hier umgesetzt: Der Mensch war hier in der Lage, eine KI zu schreiben, die solche Dinge tun kann.

Der Mathematiker Lothar Sebastian Krapp ist Lecturer am Institut für Interdisziplinäre Sprachevolutionswissenschaft der Universität Zürich. Er ist zugleich Privatdozent am Fachbereich Mathematik und Statistik der Universität Konstanz. Auf campus.kn sprach er zuvor über die mathematischen Grenzen von Künstlicher Intelligenz.