Was angekündigt wurde
Am 26. Oktober erklärte OpenAI, ein nicht veröffentlichtes internes Modell habe ein 67-seitiges Manuskript mit dem Titel The Exponential Time Hypothesis is False erzeugt, datiert auf den 17. Oktober und überarbeitet am 25. Die Behauptung: ein deterministischer Algorithmus, der die erfüllenden Belegungen jeder k-CNF-Formel in polynomiellem Speicher und in einer Zeit in der Größenordnung von 2^(n/(log n)^(1/2)) zählt. Das ist subexponentiell und würde damit die Exponentialzeithypothese widerlegen – die Vermutung von Russell Impagliazzo und Ramamohan Paturi aus dem Jahr 2001, dass 3-SAT mit n Variablen im schlechtesten Fall 2^Ω(n) Zeit braucht – und, so argumentiert das Papier, auch die Strong Exponential Time Hypothesis.
Das Papier benennt seine Grenzen ausdrücklich: Es behauptet nicht, dass NP-Probleme allgemein subexponentielle Algorithmen zulassen, und es entscheidet P gegen NP nicht.
Wie es entstand
Als einziger Autor ist „OpenAI" genannt. Die README des Repositories erklärt, die „überwiegende Mehrheit der Ergebnisse" sei mit demselben internen Modell erzielt worden, bei durchschnittlich „drei Stunden ChatGPT-Pro-Denk-Compute" pro Ergebnis, und die Manuskripte seien „am besten als eine Form von Rohforschungsdaten zu verstehen, nicht als polierte akademische Arbeiten". OpenAI zufolge entstand der natürlichsprachliche Widerlegungsbeweis am 16. Oktober und wurde am Folgetag in Lean formalisiert.
Eine Maschinenprüfung ist keine Validierung. Lean bestätigt, dass die formale Aussage aus ihren Annahmen folgt; ob diese formale Aussage die eigentliche Behauptung des Papiers einfängt, bleibt eine Frage für Fachleute. OpenAIs eigene Lean-Notizen verzeichnen eine etwas schwächere Zeitschranke als die schärfste im Manuskript – eine Lücke, die gerade deshalb zählt, weil das ganze Argument davon abhängt, unter die Exponentialkurve zu kommen.
Das Prüfarrangement – und warum es umstritten ist
OpenAI zufolge soll die Arbeit von einer Gruppe unter Leitung von Impagliazzo und Paturi (UC San Diego) sowie Ryan Williams (MIT) „verifiziert und begleitet" werden. Alle drei unterzeichneten einen offenen Brief: „Unsere Beteiligung sollte nicht als Zertifizierung der Behauptung verstanden werden. Ein Ergebnis dieser Tragweite verlangt sorgfältige, unabhängige Prüfung." OpenAI verpflichtete sich, eine Konferenz zu finanzieren, und erklärt, Teilnehmer müssten keine Geheimhaltungsvereinbarungen unterschreiben.
Umstritten bleibt das Verfahren trotzdem. Ein Beratergremium aus Mathematikern, das OpenAI nach früheren Proof-Veröffentlichungen einberufen hatte, empfahl KI-Firmen, die Praxis nicht zu übernehmen, ausgewählten Forschern Erstzugriff zu geben – genau diese Praxis wird hier wiederholt.
Zwei weitere Behauptungen, dünnere Belege
Dieselbe Ankündigung beansprucht einen Beweis der Local-Smoothing-Vermutung in jeder Dimension, der laut OpenAI die Kakeya-Vermutung löst (in drei Dimensionen 2025 von Hong Wang und Joshua Zahl bewiesen). Hinzu kommt ein Existenzbeweis für die Quantenchromodynamik – das Yang-Mills-Problem, die Hälfte eines Clay-Millennium-Preises. Die Materialien dazu wurden nicht veröffentlicht; damit ist dies die am schlechtesten prüfbare der drei Behauptungen.
Warum es zählt
Hält das ETH-Ergebnis, fällt eine tragende Annahme hinter Hunderten Arbeiten der feinkörnigen Komplexitätstheorie, und die Härte des exakten SAT-Zählens muss neu hergeleitet werden. Hält es nicht, bleibt die Episode dennoch ein Beleg dafür, wie Frontier-Labore Mathematik heute publizieren: Preprint per Pressemitteilung, Formalisierung als Glaubwürdigkeitsbeleg, Peer Review als Nachgedanke.
Praktisch ist der Effekt vorerst nahe null. Ein sich als SAT-Fachmann bezeichnender Kommentator auf Hacker News nannte die Schranken „galaktisch" – keine unmittelbaren Anwendungen, aber womöglich Ideen, die Jahre später in schnellere Solver münden. OpenAI selbst räumt ein, die Umwandlung in praktische Verbesserungen erfordere „erhebliche weitere Forschung".
Der eigentliche Test ist die laufende unabhängige Prüfung, nicht der bestandene Lean-Build.
