Zwei KI-Labore widerlegen eine Vermutung von 1999. Warum der Prüfweg die eigentliche Nachricht ist

TL;DR. Am 26. Oktober hat OpenAI gemeldet, ein internes Modell habe die Exponentialzeit-Hypothese widerlegt. Die Vermutung der Informatik stammt von 1999, Hunderte Fachartikel bauen auf ihr auf. Stunden später legte Anthropic einen eigenen Beweis vor, gefunden von einem internen Claude-Modell ohne menschliches Zutun. Beide Labore fanden ihren Beweis am 16. Oktober, beide liefern ihn mit einer Prüfung im Beweisprogramm Lean. Fachleute prüfen noch, und für die Praxis ändert sich vorerst nichts. Für Unternehmen zählt der Prüfweg: KI liefert jetzt Ergebnisse auf Forschungsniveau, und die besten kommen mit einer Prüfung, die jeder Rechner nachrechnen kann. Wir haben das mit Anthropics Beweis auf einem Mac getan.

Was die beiden Labore melden

Die Vermutung betrifft ein Grundproblem der Informatik. Eine Formel aus Ja-nein-Schaltern soll so belegt werden, dass alle Bedingungen erfüllt sind. Wer jede Belegung durchprobiert, verdoppelt den Aufwand mit jedem weiteren Schalter. Seit den 1980er-Jahren haben Forschende diesen Aufschlag gedrückt, zuletzt auf knapp 31 Prozent je Schalter. Die Hypothese von Russell Impagliazzo und Ramamohan Paturi sagt: Ganz verschwinden kann er nie.

Beide Papiere behaupten das Gegenteil. OpenAIs Arbeit hat 67 Seiten, Anthropics Arbeit 49. Beide beschreiben ein Verfahren, dessen Aufschlag je Schalter mit wachsender Formel gegen null sinkt. Laut Anthropic brauchte das Modell dafür 14 Millionen Token Ausgabe.

OpenAI legte am selben Tag zwei weitere Ergebnisse vor. Eines beweist eine Vermutung von 1991 über die Bündelung von Wellen, aus der auch die bekannte Kakeya-Vermutung folgt. Das andere ist ein Existenzbeweis für die Quantenchromodynamik, die Theorie der starken Kernkraft, und berührt eines der Millennium-Probleme der Mathematik. Diese Unterlagen sind noch nicht öffentlich. Eine Gruppe um den Nobelpreisträger David Gross prüft sie. Laut OpenAIs Ankündigung stammt alles von einem unveröffentlichten Modell, dem rund 4.000 offene Probleme gestellt wurden, mit im Schnitt drei Stunden Denkzeit je Ergebnis.

Der Haken

• Unabhängig bestätigt hat es noch niemand. OpenAIs Beweis prüft eine Gruppe um Impagliazzo, Paturi und Ryan Williams vom MIT, OpenAI bezahlt dazu eine Konferenz. Williams nannte OpenAIs Massenveröffentlichung von Anfang Oktober laut TechCrunch einen „DDoS-Angriff auf Mathematiker“.
• Lean prüft den Beweis, nicht die Frage. Das Programm bestätigt, dass die Schlusskette lückenlos ist. Ob die Aussage in Lean genau die gemeinte Vermutung trifft, prüft keine Maschine. Anthropic schreibt das selbst und hält die entscheidende Datei deshalb kurz.
• Fehler kommen vor. Am 7. Oktober zog OpenAI drei Manuskripte wegen eines Vorzeichenfehlers zurück und überarbeitete 14 weitere. Formal geprüft sind laut OpenAI rund 42 Prozent der Hauptergebnisse.
• Für die Praxis wertlos, sagen die Autoren selbst. Anthropic rechnet vor, ab welcher Größe das Verfahren schneller ist als stures Durchprobieren.

Wir haben nachgerechnet

Anthropic beschreibt, wie man den Beweis selbst prüft. Wir haben das am 28. Oktober auf einem MacBook Pro mit Apple M4 Max getan: Lean installiert, die vorgefertigte Mathematik-Bibliothek geladen, den Beweis übersetzen lassen. Das Laden der Bibliothek dauerte 5:36 Minuten, das Übersetzen und Prüfen des Beweises 8:54 Minuten. Anthropic nennt für einen Server mit 24 virtuellen Prozessoren etwa acht Minuten. Am Ende stehen zwei Zeilen: Beide Hauptsätze hängen nur an Leans drei Standard-Axiomen. Kein Schritt wurde ausgelassen, keine Annahme versteckt.

Was das nicht zeigt: ob die Aussage die Vermutung wirklich trifft. Dafür braucht es weiter Fachleute. Aber der aufwendigste Teil der Prüfung ist keine Vertrauensfrage mehr, sondern eine Rechnung, die jeder wiederholen kann.

Was das für den Mittelstand heißt

Kurzfristig nichts. Planungs-, Konfigurations- und Prüfsoftware rechnet weiter wie bisher. Solche Werkzeuge leben davon, dass echte Formeln eine Struktur haben, und nicht vom ungünstigsten Fall, um den es hier geht. Auch Verschlüsselung bleibt, wie sie ist: OpenAI hat laut Williams geprüft und ist ziemlich sicher, dass daraus keine Brüche folgen.

Wichtiger ist, was die Meldung über die Werkzeuge sagt. Zwei Labore haben unabhängig voneinander eine Annahme gekippt, die 27 Jahre als sicher galt. Und beide haben gewartet, bis eine Maschine den Beweis prüfen konnte. Dieses Muster lässt sich übertragen: Ergebnis plus Prüfweg. Bei Code sind das Tests, bei Berechnungen eine Gegenrechnung, bei Konstruktionen eine Simulation oder Messung. Je mehr die Modelle liefern, desto weniger schaffen Menschen, alles von Hand zu lesen. Laut Anthropic kann schon das öffentlich verfügbare Claude Opus 5.5 die Widerlegung aus einer kurzen Skizze herleiten. Wie das bei Software aussieht, haben wir in „Bewiesen statt getestet“ beschrieben.

Was Sie jetzt tun sollten

1. Nichts umbauen. Keine Verschlüsselung und keine Planungssoftware muss wegen dieser Meldung geändert werden.
2. Den Prüfweg vor den Auftrag stellen. Legen Sie fest, wie ein KI-Ergebnis maschinell geprüft wird, bevor Sie es anfordern: Tests, Gegenrechnung, Grenzwerte, Simulation.
3. Prüfzeit einplanen. Eine KI liefert in Stunden, woran Fachleute wochenlang lesen. Planen Sie Ihre Fachleute für die Abnahme ein, nicht nur für die Erstellung.
4. Ein offenes Problem aufschreiben. Eine Toleranzrechnung, eine Planungsregel, ein Messfehler, den niemand erklären kann. Mit einem Prüfkriterium dazu ist es ein guter erster Test für die heutigen Modelle.
5. Das Urteil der Prüfgruppe abwarten, bevor Sie sich in Angeboten oder Strategiepapieren auf die Widerlegung berufen.

Die Mathematik ist neu, das Prinzip nicht: Was eine Maschine prüfen kann, muss niemand glauben. Wenn Sie für einen ersten Anwendungsfall den Prüfweg gleich mitdenken möchten, sprechen Sie uns gern an.