OpenAI veröffentlicht 722 Mathe-Manuskripte - Prüfquote unklar

Ein Repository taucht um 21:47 Uhr auf

Am 6. Oktober, 21:47 Uhr UTC, erscheint auf GitHub ein Repository namens openai/math. Darin: 722 mathematische Manuskripte, erzeugt von einem internen OpenAI-Modell, auf das niemand von außen Zugriff hat. Vierzehn Minuten später landet die letzte Datei. Am Tag danach knackt das Repository die Marke von 8.500 Sternen.

Die Presse titelt mit zwei verschiedenen Zahlen: The Decoder spricht von 372 Ergebnissen, unite.ai von 722. Beide haben recht - das README löst den Widerspruch in einem Satz: „722 Manuskripte, organisiert in 372 Familien.“

Eine Familie fasst Papiere zusammen, die um dasselbe Ergebnis kreisen: sein Hauptargument, seine Folgerungen, alternative Beweiswege. Familien oder Papiere zu zählen ist wie Kisten oder Flaschen zu zählen.

Das Wort, das die Zahl ersetzt hat

Offen bleibt, was weder 722 noch 372 beantworten: Wie viele dieser Beweise kann eine Maschine tatsächlich prüfen?

OpenAIs Ankündigung sagt es nicht. Sie teilt „Formalisierungen vieler Beweise“ in Lean, „einer Programmiersprache, mit der mathematische Beweise von einem Computer verifiziert werden können“. Vieler. Das Wort übernimmt die Rolle einer Zahl - wie ein Etikett, das Früchte verspricht, ohne den Anteil zu nennen.

Formalisieren heißt, einen Beweis in eine Sprache zu übertragen, die nichts durchgehen lässt: keine Intuition, kein „das sieht man leicht“. Fehlt ein Schritt, kompiliert es nicht. Daher das Gewicht dieser Zahl - der einzige Wert im Repository, der etwas über die Tragfähigkeit des Ganzen aussagt.

Beide Berichte, so uneins bei 722 und 372, übernehmen das „vieler“ unverändert, ohne je eine Zahl zu nennen. Nur ein Fachmedium hat sie gesucht und veröffentlicht, mit Verweis auf die Quelldatei. Nur erzählt diese Datei nicht alles.

Was eine solche Prüfung wert ist, haben wir hier schon einmal gezeigt: Am 8. September war es ein in Lean kontrollierter Beweis, der verhinderte, dass eine seit 1934 offene Frage vorschnell als gelöst galt.

162 - und warum es nicht 44 Prozent sind

Eine Datei liefert die Antwort: lean/formalization.yaml, Version 0.4, deren Kopfzeile sich selbst als „Katalog der Papiere mit formalisiertem Hauptresultat“ bezeichnet. Sie zählt 162 Einträge, jeder verweist auf ein Manuskript.

162 von 722 Manuskripten, also 22 Prozent zum Stichtag 7. Oktober. Das Datum zählt: Die Datei ist versioniert, und OpenAI kündigt an, weitere Einträge nachzureichen.

Eine schmeichelhaftere Zahl kursiert: 162 von 372 Familien, also 44 Prozent. Sie ist falsch, und zwar deutlich. Die 162 Einträge bezeichnen Papiere, keine Familien, und 23 Familien stellen mehrere davon - Familie 331 allein kommt auf sieben formalisierte Papiere. Papiere im Zähler, Familien im Nenner: Das ist, als teilte man Äpfel durch Kisten.

Die Zählung nach Familien haben wir selbst gemacht: Diese 162 Papiere decken 127 von 372 Familien ab, also 34 Prozent zum selben Stichtag.

Der offizielle Katalog übersieht Beweise

Doch das Repository führt ein zweites Register, und das erzählt eine andere Geschichte. In der Manuskript-Übersicht verweisen 235 von 372 Familien auf ein Blatt, das den Umfang ihrer Lean-Formalisierung beschreibt, und genau 235 solcher Blätter liegen auch im entsprechenden Ordner. Der Katalog selbst deckt davon nur 127 ab.

Einhundertacht Familien besitzen also ein Lean-Blatt, ohne im Formalisierungskatalog zu erscheinen. Der umgekehrte Fall kommt nie vor.

Nehmen wir Familie 005, die Irrationalität der Catalan-Konstante. Ihr Blatt ist eindeutig: „Die Formalisierung beweist, dass die Catalan-Konstante ... irrational ist. Das ist die mathematische Aussage im Titel des Papers.“ Die Datei Catalan.lean existiert tatsächlich, das Wort „Catalan“ taucht in formalization.yaml aber kein einziges Mal auf.

Zwölf dieser 108 Blätter wurden einzeln geöffnet. Alle zwölf beschreiben eine Formalisierung des Hauptresultats, vom Irrationalitätsmaß von π bis zur Erdős-Vermutung über Summen von Kehrwerten. Keine Entwürfe.

162 ist damit eine Untergrenze: Das offizielle Register ist kürzer als das Regal, das es beschreiben soll.

„Formalisiert“ heißt nicht „geprüft“

Noch eine Lücke, in die andere Richtung. Man liest bereits, 162 Beweise seien „von Lean verifiziert“ worden. Veröffentlicht hat diese Prüfung niemand.

Was OpenAI liefert, sind 405 Aussagen-Dateien und eine Anleitung, sie selbst zu kompilieren. Das Repository enthält keine kontinuierliche Integration: Keine Prüfung läuft automatisch, und das README der Lean-Bibliothek warnt, alles auf einmal zu kompilieren könne scheitern - man solle „jeweils nur kleine Abschnitte“ übersetzen. OpenAI reicht den versiegelten Umschlag samt Brieföffner, ohne zu sagen, was drinsteht.

Wir ebenfalls nicht: Wir haben Dateien gezählt und OpenAIs Umfangsbeschreibungen gelesen, aber keinen einzigen Beweis kompiliert. Und diese 405 Dateien sind keine 405 Ergebnisse - eine einzige Familie kann allein vier davon beanspruchen.

Zu den 560 Manuskripten ohne Katalogeintrag schreibt OpenAI einen Satz, den die Berichte nicht übernommen haben: „Einige der nicht formalisierten Ergebnisse könnten Probleme aufweisen.“

Zwei Ergebnisse fallen aus dem Rahmen

Das README beschreibt die Entstehung: etwa 4.000 gestellte Probleme, rund drei Stunden Rechenzeit mit ChatGPT Pro pro Ergebnis, und eine Auswahl, die zu diesem Katalog führte.

Zwei Ergebnisse entgehen diesem Verfahren, und das Dokument sagt es offen: die nullstellenfreie Region der Riemannschen Zetafunktion und die Hodge-Vermutung für abelsche CM-Varietäten sind „Ausnahmen von diesem festen Verfahren“. Bei der ersten ergänzt OpenAI, der Text sei „von einem Menschen redigiert“ worden. Die beiden prestigereichsten Ergebnisse des Katalogs ähneln also am wenigsten dem Rest der Produktion.

Das zitierte Gremium hat das Gegenteil einer Bestätigung veröffentlicht

OpenAI erklärt, sich bei der Form dieser Veröffentlichung an den öffentlichen Empfehlungen eines unabhängigen Beratungsgremiums für Mathematik und KI orientiert zu haben, beheimatet am Institute for Advanced Study. Am selben Tag veröffentlichte dieses Gremium, die AGMAI, einen eigenen Text zur Veröffentlichung - und der beginnt mit einer Zurückweisung: „Die beratende Rolle der AGMAI darf nicht als Urteil über die Bedeutung dieser Ergebnisse oder als Billigung des Verfahrens verstanden werden, mit dem OpenAI sie erzielt hat.“

Der Text fügt hinzu, diese Veröffentlichung sei „der Anfang, nicht der Abschluss“ des menschlichen Verständnisprozesses, und es sei an der mathematischen Gemeinschaft, darüber zu urteilen. Er spricht von konstruktiven Gesprächen und begrüßt OpenAIs Dialogbereitschaft.

Noch deutlicher wird es bei den eigenen Empfehlungen der AGMAI vom 29. September, auf die sich die Ankündigung beruft. Sie beginnen mit einer Forderung, die diese Veröffentlichung gerade nicht erfüllt: „Wir billigen diese Praxis nicht und fordern sie auf, das Testen fortgeschrittener mathematischer Probleme an proprietären Modellen einzustellen.“ Die 722 Manuskripte stammen exakt aus einem solchen, nicht veröffentlichten internen Modell. OpenAI erklärt, an einer Veröffentlichung zu arbeiten.

Die neun Mitglieder der AGMAI erhalten kein Honorar: Sie gründeten diese unabhängige Struktur, nachdem OpenAI einige von ihnen für ein hauseigenes Gremium angefragt hatte. Timothy Gowers, Fields-Medaillengewinner, und Edward Witten gehören dazu.

Nicht zu verwechseln mit dem Text von fünfundzwanzig Fields-Medaillengewinnern vom 11. September, über den hier bereits berichtet wurde: Jener nennt keine Unternehmen und äußert sich nicht zur Gültigkeit eines Beweises. Zwei Dokumente, zwei Reichweiten - mit nur einem Mann in beiden: Martin Hairer, Fields-Medaillengewinner 2014, Unterzeichner der Erklärung und Mitglied des Gremiums. Nicht widersprechen heißt nicht zustimmen, und zitiert zu werden heißt nicht, zu bestätigen.