Physical Superintelligence, kurz PSI, hat am 6. November einen Beweis der Aaronson-Ambainis-Vermutung veröffentlicht. Gefunden hat ihn nach Angaben des Unternehmens ein intern entwickeltes Forschungssystem, das Instanzen eines nicht veröffentlichten Anthropic-Modells auf PSIs eigener Infrastruktur laufen ließ. Die Vermutung ist seit 2008 offen und gilt als eine der zentralen Fragen der Quantenkomplexitätstheorie.
Die Frage dahinter ist alt und praktisch zugleich: Wann sind Quantencomputer wirklich exponentiell schneller? Shors Faktorisierungsalgorithmus von 1994 ist es, weil die Eingabe ein verstecktes Muster hat, das der Algorithmus ausnutzt. Ob dieser Vorsprung auch bei zufälligen Eingaben bleibt, wo es solche Muster fast nie gibt, wusste niemand.
Was jetzt bewiesen ist
Scott Aaronson und Andris Ambainis hatten die Frage in reine Mathematik übersetzt. Ihre Vermutung sagt, dass jedes beschränkte Polynom niedrigen Grades mindestens eine Variable mit großem Einfluss hat. Aus ihr folgt: Bei Ja-Nein-Fragen über zufällige Eingaben kann ein gewöhnlicher Computer die Antwortwahrscheinlichkeit eines Quantenalgorithmus nachrechnen, und zwar mit polynomiell statt exponentiell vielen Blicken auf die Daten.
Gezählt werden dabei nur diese Blicke, nicht die gesamte Rechenzeit. Für Probleme mit passender Struktur bleibt ein exponentieller Quantenvorteil also weiter möglich. Was fällt, ist die Hoffnung auf den Vorteil ohne Struktur.
Der Beweis folgt einem Plan von Shachar Lovett und Jiapeng Zhang, ersetzt aber eine Ungleichung, die bei den beiden nur Vermutung war, durch eine neue All-Pairs-Ungleichung, und verschärft dafür David Reimers Butterfly-Lemma.
Wer hier was geprüft hat
Das ist der interessantere Teil. PSI schreibt, das System habe den vollständigen Beweis am dritten Tag des Laufs gehabt, und Lean habe ihn angenommen. Danach durfte es an verwandten offenen Problemen weiterarbeiten und hat das Ergebnis zweimal verbessert, bis Lean die finale Fassung akzeptierte.
Die formale Entwicklung enthält laut dem Audit im Repository keine Platzhalter und keine zusätzlichen Axiome. Die Deklarationen wurden durch Leans Kernel und durch lean4lean geschickt, eine unabhängige Implementierung des Typcheckers. In einem Sandbox-Lauf nahm ein Vergleicher aus den Kerneln nanoda und Lean die vier finalen Theoreme an und wies auf einem zweiten Rechner vier absichtlich falsche Lösungen zurück.
Die Grenzen stehen daneben: Dass die formale Aussage der gedruckten Vermutung entspricht, muss ein Mensch prüfen. Der lesbare Aufsatz selbst ist nicht maschinengeprüft. Leans Kernel, Leans Compiler, Mathlibs Definitionen und die benutzten Rechner bleiben Teil der vertrauten Basis.
David Turturean aus PSIs technischem Personal hat das System gebaut, das Problem umrissen, den ersten Entwurf geprüft und übernimmt die Verantwortung für die Richtigkeit. Erzeugt haben die mathematischen Aussagen, den Entwurf und die Lean-Formalisierung laut Repository KI-Modelle. Jim Halverson hat auditiert, Phiala Shanahan die Formalisierung kommentiert.
Das Urteil kommt von den Leuten, die daneben gearbeitet haben
Im August 2026 hatten Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan von Stanford einen Spezialfall erledigt: kein exponentieller Vorsprung bei zufälligen Eingaben für Quantenalgorithmen mit festgelegter Zahl paralleler Runden. Genau diese Gruppe liest den neuen Beweis, hat Kommentare geschickt und schreibt eine kürzere Fassung für Fachleute. Ihr Urteil, von PSI zitiert: „This is a huge result.“
Das ist die Bestätigung, die zählt, und sie steht bisher nur in PSIs eigenem Beitrag. Bis eine unabhängige Veröffentlichung nachzieht, ist das hier eine sehr gut belegte Behauptung und kein Lehrbuchsatz. Bemerkenswert bleibt sie auch so: Das Modell, das den Beweis gefunden hat, kann niemand von außen anfassen.