Die Riemann-Hypothese ist seit über 150 Jahren offen. Es geht um die Verteilung der Primzahlen, und wer einen allgemeinen Beweis liefert, kassiert eine Million Dollar aus dem Millennium-Preistopf des Clay Mathematics Institute. Der Topf ist noch voll.
Anthropic hat das Rätsel nicht geknackt. Aber am Montag hat das Unternehmen berichtet, dass ein bislang unveröffentlichtes Modell überraschend weit gekommen ist: Es hat die untere Schranke, bis zu der die Hypothese nachweislich gilt, deutlich nach oben geschoben. Für ein Problem dieser Größenordnung ist das mehr, als die meisten von einem Sprachmodell erwartet hätten.
Wie das ablief
Der spannendste Teil ist nicht das Ergebnis, sondern der Weg dahin. Ein Anthropic-Mitarbeiter ohne nennenswerte Mathe-Ausbildung hat das Modell gebeten, einen „echten Versuch” zu wagen, die Hypothese zu beweisen – und es dann anderthalb Tage lang allein weiterarbeiten lassen.
In dieser Zeit hat das Modell 650 verschiedene Ansätze durchgespielt, verteilt auf 60 Subagenten, und dabei 31 Millionen Output-Token verbraucht. Eine Fußnote im Paper schlüsselt die Arbeitsteilung auf: Zwei der 60 Subagenten haben die entscheidenden mathematischen Ideen entwickelt, 13 haben ihnen zugearbeitet, 30 haben es versucht und sind gescheitert, 13 haben als Prüfer die Argumente auf Korrektheit gecheckt, und zwei haben am Ende das erste Paper geschrieben.
Bestätigt wurde der Fortschritt von zwei hauseigenen Mathematikern. Formalisiert haben sie ihn mit Lean, dem quelloffenen Beweisassistenten.
Kein Einzelfall mehr
Das reiht sich in eine ganze Serie ein. Über das Jahr haben KI-Modelle mehrere Erdős-Probleme gelöst. OpenAI hat kürzlich zehn Resultate seines internen Modells „Astra” vorgestellt, und Anthropic selbst hatte davor schon die Jacobi-Vermutung widerlegt. Die Modelle werden besser, die Ergebnisse werden dicker.
In der Mathematik löst das gemischte Gefühle aus. Im Juni haben prominente Mathematiker die Leiden-Deklaration unterschrieben, aus Sorge, dass KI ein Kernprinzip des Fachs aushöhlt: dass ein Beweis einem Menschen zugeschrieben wird, der die Verantwortung dafür trägt. Fields-Medaillen-Träger Timothy Gowers hat darauf in einem Blogpost geantwortet – und die Sache offener gesehen. Vielleicht, schreibt er, sei eine Welt, in der Sätze nicht mehr an bestimmte Mathematiker gebunden sind, am Ende gar nicht so schlimm. Sterne seien schließlich auch nicht nach Astronomen benannt, und die meisten trügen überhaupt keinen Namen.
Meine Einordnung
Mich fasziniert an der Geschichte weniger das Mathe-Ergebnis – das können ohnehin nur Fachleute wirklich beurteilen. Es ist das Setup. Ein Mensch ohne Mathe-Hintergrund tippt „nimm dir das mal richtig vor”, geht schlafen, und anderthalb Tage später liegt ein Fortschritt bei einem Jahrhundertproblem auf dem Tisch, geprüft und in Lean formalisiert.
Genau das ist der Punkt, an dem diese Werkzeuge kippen: von „hilft mir beim Formulieren” zu „arbeitet ein Problem eigenständig durch, das ich selbst nicht mal ansatzweise lösen könnte”. Ob am Ende ein Name unter dem Beweis steht, ist dann fast schon die kleinere Frage. Die größere ist, was wir mit anderthalb Tagen und 60 Subagenten sonst noch angehen könnten.
Quellen: