PSI: Ein KI-System findet einen Lean-Beweis für die Aaronson-Ambainis-Vermutung

Physical Superintelligence (PSI) hat am 6. November 2026 bekannt gegeben, dass ein internes Forschungssystem, angetrieben von Instanzen eines nicht öffentlichen Anthropic-Modells, einen Beweis für die seit 2008 offene Aaronson-Ambainis-Vermutung gefunden hat. Nach Angaben des Labors akzeptierte Lean am dritten Tag des Durchlaufs einen vollständigen Beweis, gefolgt von zwei Verbesserungen. Das Manuskript und die Lean-4-Formalisierung sind öffentlich zugänglich.

Was die Vermutung besagt

Scott Aaronson und Andris Ambainis untersuchten die Frage, ob ein Quantencomputer eine Ja/Nein-Frage auf einer zufälligen Zeichenkette mit exponentiell weniger Lesezugriffen beantworten kann als ein klassischer Computer. Die meisten bekannten spektakulären Beschleunigungen (wie der Shor-Algorithmus) beruhen auf einer seltenen Struktur in der Eingabe. Ihre Vermutung aus der reinen Mathematik impliziert, sofern sie zutrifft, dass bei Fehlen einer solchen Struktur der klassische Mehraufwand bezogen auf die Anzahl der Quanten-Lesezugriffe höchstens polynomiell bleibt.

Konkret ist nach T Lesezugriffen die Wahrscheinlichkeit, dass ein Quantenalgorithmus „Ja“ sagt, ein Polynom vom Grad höchstens 2T mit Werten in [0, 1]. Die Vermutung besagt, dass ein solches Polynom, wenn es hinreichend variiert, stets eine Variable mit ausreichend großem Einfluss besitzt — was es einem klassischen Computer ermöglicht, die Vorhersage zu imitieren, indem er nur wenige Bits betrachtet.

Was PSI veröffentlicht

Die Forschungsseite und das GitHub-Repository beschreiben einen Beweis, der einem Konzept von Lovett und Zhang folgt und eine Ungleichung ersetzt, die diese offen gelassen hatten. Das README nennt vier Lean-Theoreme ohne Platzhalter oder hinzugefügte Axiome, die von zwei Implementierungen des Lean-Kernels (Versionen 4.33.0 / Mathlib v4.33.0, Apache-2.0-Lizenz) erneut überprüft wurden. David Turturean leitete die Arbeit; Jim Halverson prüfte den Beweis; Phiala Shanahan kommentierte die Formalisierung.

Im August 2026 hatten vier Forscher aus Stanford (Blanc, Docter, Strassle, Tan) bereits einen Spezialfall gelöst. PSI gibt an, dass diese nun den vollständigen Beweis lesen und eine kürzere Darstellung vorbereiten; das Labor zitiert einen lobenden Kommentar von ihnen.

Einschränkungen, die man im Kopf behalten sollte

Das Repository überlässt es dem Leser zu überprüfen, ob die Lean-Aussage PrintedConjecture tatsächlich der gedruckten Vermutung entspricht. Ein verbessertes Theorem stützt sich auf eine Hypothese von Agarwal und Ben-David, die hier nicht formalisiert ist. Das Prosapapier ist nicht maschinell geprüft. Das Anthropic-Modell wird weder benannt noch ist es öffentlich: Man kann das Resultat untersuchen, den Entdeckungsprozess jedoch nicht nachspielen. Zum Zeitpunkt unserer Berichterstattung lag keine öffentliche Reaktion von Aaronson oder Ambainis vor.