Ein internes OpenAI-Modell hat nach Angaben des Unternehmens einen Algorithmus gefunden, der die Exponential Time Hypothesis widerlegt, eine seit rund 25 Jahren genutzte Grundannahme der Informatik. Der Beweis ist im Beweisassistenten Lean maschinell geprüft. Ob er das Richtige beweist, klären jetzt die Urheber der Hypothese selbst.
Ein Klick · kostenlosDr. Web bei Google bevorzugenMarkieren Sie drweb.de als bevorzugte Quelle. Dann sehen Sie unsere Artikel öfter unter den Top-Meldungen.Jetzt hinzufügenHunderte Fachaufsätze begründen mit dieser Annahme, warum sich bestimmte Probleme nicht schnell lösen lassen. Am Montagabend hat OpenAI sie für falsch erklärt und zwei Ergebnisse aus Mathematik und Physik vorgelegt.[1] Stand: Dienstag, 1:30 Uhr. Offen ist, ob die unabhängige Prüfung den Beweis bestätigt.
Das Wichtigste in Kürze
- OpenAI meldet einen Algorithmus, der die Lösungen von 3-SAT-Formeln in subexponentieller Zeit zählt. Damit wäre die Exponential Time Hypothesis widerlegt.
- Das Modell fand den Beweis am 16. Oktober, einen Tag später lag er in Lean formalisiert vor.
- Prüfen werden ihn Russell Impagliazzo und Ramamohan Paturi, zwei Urheber der Hypothese, und Ryan Williams.
- Für Verschlüsselung und heutige SAT-Solver ändert sich vorerst nichts.
Was besagt die Exponential Time Hypothesis?
Die Hypothese betrifft das Erfüllbarkeitsproblem der Aussagenlogik, kurz SAT: Lassen sich die Variablen einer Formel so auf wahr oder falsch setzen, dass alle Bedingungen erfüllt sind? Für die Variante 3-SAT, in der jede Bedingung höchstens drei Variablen verknüpft, besagt die Exponential Time Hypothesis (ETH): Kein Algorithmus schafft das in subexponentieller Zeit.[2]
In der Forschung dient die Annahme als Werkzeug. Zeigt jemand, dass ein schnelles Verfahren für ein Graphenproblem auch 3-SAT schnell lösen würde, gilt das Graphenproblem als schwer, sofern die ETH stimmt. Fällt die ETH, verlieren solche Arbeiten ihre Begründung. Falsch werden ihre Aussagen dadurch nicht automatisch.
Was hat OpenAIs Modell gefunden?
Laut der Lean-Fassung zählt ein deterministischer Algorithmus exakt, wie viele Belegungen eine Formel erfüllen, solange jede Bedingung höchstens eine feste Zahl von Variablen enthält. Dafür braucht er nur polynomiellen Speicher. Im Exponenten der Rechenzeit steht die Variablenzahl n, multipliziert mit einer Konstanten und dem Bruch (log log n)² geteilt durch die Wurzel aus log n.[3] Weil dieser Bruch mit wachsendem n gegen null geht, ist die Laufzeit subexponentiell.
Praktisch hilft das nicht: Bei einer Million Variablen liegt der Bruch noch bei 1,86. Unter eins fällt er erst, wenn die Zahl der Variablen mehr als 2.000 Stellen hat. OpenAI schreibt selbst, bis zu schnelleren Verfahren in der Praxis sei noch erhebliche Forschung nötig.[1]
Lean prüft jeden Beweisschritt maschinell, aber nur gegen die formale Aussage. Ob diese Aussage mit ihrem eigenen Maschinenmodell und ihrer Kodierung der Formeln die ETH tatsächlich trifft, müssen Menschen nachvollziehen. Diese Prüfung übernehmen Impagliazzo und Paturi von der UC San Diego sowie Williams vom MIT. Auf ihren Wunsch hat OpenAI alle Rohdaten veröffentlicht und eine Fachkonferenz zugesagt.[1]
Am 7. Oktober zog OpenAI drei mathematische Manuskripte zurück, weil ein Vorzeichenfehler eine ganze Beweiskette gekippt hatte.[4] Einen Lean-Beweis hatten diese Arbeiten nicht. Der Navier-Stokes-Beweis vom September betraf nur eine Variante des Millennium-Problems.
Ein maschinell geprüfter Beweis ist noch kein verstandener. Diese Arbeit leisten weiterhin Fachleute.
Michael Dobler, Herausgeber Dr. Web
Wie OpenAI die drei Ergebnisse herausgibt
Was bedeutet das für Verschlüsselung und SAT-Solver?
Gängige Verschlüsselung wie RSA oder die vom BSI empfohlenen gitterbasierten Verfahren beruhen auf anderen mathematischen Problemen als 3-SAT. Auch die Frage, ob P gleich NP ist, bleibt offen: Eine subexponentielle Laufzeit ist immer noch langsamer als jede polynomielle.
SAT-Solver, die in der Industrie Chipentwürfe und Produktkonfigurationen prüfen, lösen Praxisformeln mit Heuristiken. An ihnen ändert der neue Algorithmus nichts. Für Entscheider heißt das:
- Sicherheitskonzepte nicht umstellen: Der gemeldete Algorithmus gibt Angreifern kein neues Werkzeug.
- KI-Ergebnisse im eigenen Haus an eine maschinelle Gegenprüfung koppeln, bei Code etwa über formale Verifikation, wie sie Mistral mit Leanstral anbietet.
Quellen
4 Quellen anzeigenQuellen ausblenden
- OpenAIWorking with academic communities to build scientific understanding
- Russell Impagliazzo, Ramamohan PaturiOn the Complexity of k-SAT (Journal of Computer and System Sciences, Band 62, 2001)
- OpenAI, GitHub-Repository openai/mathSubexponentialSAT.lean (formale Aussage des Beweises, Stand 26. Oktober 2026)
- OpenAI, GitHub-Repository openai/mathHistory (Versionshinweise vom 7. und)
Mehr Newshunger?
- OpenAI zieht drei mathematische Ergebnisse zurück
- OpenAI meldet Beweis für ein Millennium-Problem der Mathematik
- Wie KI in der Mathematik die Grundlagen des Fachs erschüttert
- Mathematiker schlagen Alarm: KI holt beim Beweisen auf
- GPT-5.6 Sol Ultra legt einen Beweis für die 50 Jahre alte Cycle-Double-Cover-Vermutung vor
- OpenAI-Modell löst 80 Jahre altes Mathematik-Problem
