Die ETH ist eine Vermutung über die grundlegende Schwierigkeit von Erfüllbarkeitsproblemen: Grob gesagt besagt sie, dass sich k-SAT für k ≥ 3 nicht in Zeit 2o(n) lösen lässt, wobei n die Anzahl der Variablen ist – es gibt also keinen Algorithmus, der alle Instanzen in subexponentieller Zeit in n löst. In der Praxis dient die ETH als Maßstab für die algorithmische Schwierigkeit: Viele bedingte untere Schranken für Graphenprobleme, Datenbankabfragen und Reduktionen aus der Computational Biology setzen die ETH voraus und folgern daraus, dass deutlich bessere Laufzeiten überraschend wären. Wenn Forschende ein Problem als ETH-schwer bezeichnen, meinen sie, dass eine drastische Verbesserung einen Durchbruch gegenüber diesem Maßstab bedeuten würde.

OpenAIs Behauptung betrifft SAT mit fester Klauselbreite: SAT-Instanzen, die durch ihre Klauselstruktur oder die Verknüpfungen zwischen Variablen eingeschränkt sind. Entwickelt jemand einen Algorithmus, der alle solchen Instanzen in Zeit 2o(n) löst – also subexponentiell in n –, widerspricht das der pauschalen Aussage der ETH über exponentielle untere Schranken für k-SAT-Familien. Damit wären zahlreiche bedingte Härteresultate hinfällig, die ausdrücklich die ETH voraussetzen. Entscheidend ist: Die ETH zu widerlegen ist nicht dasselbe, wie P = NP zu beweisen. Die ETH ist eine stärkere, spezifischere Vermutung über die genaue exponentielle Abhängigkeit der Laufzeiten. P = NP würde die Lücke zwischen polynomieller und nichtdeterministisch-polynomieller Zeit schließen. Ein subexponentieller Algorithmus für eine bestimmte SAT-Familie zeigt hingegen bessere asymptotische Laufzeiten für genau diese Familie, ohne zu behaupten, dass sich alle NP-Probleme in Polynomialzeit lösen lassen.

Einen Beweis in Lean zu formalisieren, ist ein wichtiger Schritt: Es zwingt zu präzisen Definitionen, schließt viele informelle Lücken und schafft ein maschinenprüfbares Ergebnis, das vor bestimmten Arten menschlicher Fehler schützt. OpenAIs Team berichtet, dass die Lean-Formalisierung innerhalb von 24 Stunden auf den natürlichsprachlichen Gegenbeweis folgte. Dennoch prüft formale Verifikation die syntaktische Korrektheit relativ zu den formalen Axiomen und Definitionen. Sie ersetzt nicht die Einordnung durch die Fachgemeinschaft – etwa hinsichtlich Modellannahmen, versteckter Konstanten in asymptotischen Analysen, Parameterbereichen oder der Frage, ob der Algorithmus breit anwendbar ist oder nur auf pathologische Instanzfamilien zugeschnitten wurde.

OpenAI hat eine Prüfgruppe unter der Leitung von Russell Impagliazzo und Ramamohan Paturi – zwei der ursprünglichen Urheber der ETH – sowie Ryan Williams vom MIT eingeladen. Das Trio verbindet historisches Hintergrundwissen mit großer fachlicher Expertise: Impagliazzo und Paturi können beurteilen, ob der mögliche Gegenbeweis tatsächlich der ursprünglichen ETH-Formulierung widerspricht, während Williams die Folgen für untere Schranken bei Algorithmen und verwandte bedingte Resultate bewerten kann. Ihre Leitung dürfte eine transparente, von Fachleuten geführte Prüfung des Ergebnisses unterstützen und steht beispielhaft für eine konstruktive Zusammenarbeit zwischen KI-Unternehmen und Wissenschaft.

Dieser Fall veranschaulicht einen neuen Forschungsablauf: Generative Modelle können Vermutungen aufstellen und sogar maschinenprüfbare Beweise liefern – so verkürzt sich der Weg von der Idee zum formalisierten Ergebnis. Für Forschungsteams, Förderer und Produktverantwortliche ergibt sich daraus unmittelbar: Sie sollten in Verifikationsinfrastruktur, offene Repositorien für Forschungsartefakte und finanziell unterstützte Prüfungen durch die Fachgemeinschaft investieren. Risiken bleiben bestehen: Modelle können falsche Lemmata erfinden, die sich dennoch typprüfen lassen, Definitionen falsch anwenden oder enge Annahmen zu bestimmten Instanzen ausnutzen. Die richtige Reaktion ist weder unkritische Begeisterung noch vorschnelle Ablehnung, sondern eine strukturierte, transparente Prüfung durch Fachleute.