PSI beansprucht einen Lean-formalisierten Beweis der Aaronson–Ambainis-Vermutung

Physical Superintelligence (PSI) erklärte am 6. November 2026, sein internes Forschungssystem habe einen Beweis der Aaronson–Ambainis-Vermutung erzeugt, den Lean akzeptiert habe. Das System habe dafür ein nicht öffentliches, von PSI nicht näher benanntes Anthropic-Modell verwendet, so PSIs Ankündigung. Das öffentliche PSI-Repository präzisiert den formalisierten Satz. Es hält zugleich fest, dass Menschen prüfen müssen, ob dieser Satz tatsächlich der gemeinten Vermutung entspricht.

Was die formale Aussage besagt

Die Aaronson–Ambainis-Vermutung betrifft den Einfluss einzelner Bits auf beschränkte Polynome. Das Repository formuliert sie für ein reelles Polynom mit höchstens dem Grad d, dessen Werte auf der Menge aller Bitfolgen {0,1}^N zwischen 0 und 1 liegen. Außerdem muss seine Varianz mindestens ε > 0 betragen. Varianz beschreibt hier, wie stark die Polynomwerte über gleichverteilt gewählte Bitfolgen streuen.

Für mindestens eine Koordinate gibt das Repository zwei Untergrenzen für den Einfluss an: (8√15/(125π⁴)) · ε^(5/2)/d⁶ sowie (ε/d)⁷. Der Einfluss eines Bits ist als erwarteter quadrierter Unterschied zwischen dem Polynomwert bei einer Bitfolge und seinem Wert nach dem Umklappen dieses Bits definiert. Die Aussage verbindet damit die Streuung der Werte und den Polynomgrad mit einer Untergrenze dafür, wie stark wenigstens ein einzelnes Bit den Wert beeinflusst.

Die beiden Schranken gehören zum formalisierten Satz; sie sind keine Messwerte eines Quantencomputers. Ihre Bedeutung hängt von den Voraussetzungen über Grad, Wertebereich und Varianz ab.

Bei einem maschinengeprüften Beweis sind zwei Fragen getrennt zu betrachten: Folgt der formale Satz aus dem Lean-Code, und entspricht dieser Satz tatsächlich der gemeinten Vermutung?

Was Lean prüft

Lean ist ein Beweisassistent: Seine Prüfroutine kontrolliert, ob eine formale Aussage aus den im System angegebenen Definitionen und Beweisschritten folgt. PSI gibt an, dass sein Repository vier abschließende Theoremdeklarationen enthält und die Formalisierung keine Platzhalter oder zusätzlich eingeführten Axiome verwendet. Das Repository beschreibt Prüfungen mit dem Lean-Kernel und lean4lean.

Eine solche Prüfung betrifft die formale Ableitung. Sie bestätigt nicht automatisch, dass die als PrintedConjecture bezeichnete Aussage inhaltlich genau der ursprünglichen Vermutung entspricht. Das Repository überlässt diesen Abgleich den Lesern. Auch das für Menschen lesbare Paper ist laut Repository nicht selbst vollständig maschinengeprüft. Zur Vertrauensbasis zählt es außerdem den Lean-Kernel und -Compiler, Definitionen aus Mathlib sowie die Prüfmaschinen.

Welche Folgerung PSI für Quantenabfragen beschreibt

PSI ordnet die Aussage der Quanten-Abfragekomplexität zu. In diesem Modell lässt sich die Ja-Wahrscheinlichkeit eines Quantenalgorithmus nach T Abfragen als beschränktes Polynom vom Grad höchstens 2T darstellen. PSI beschreibt als Folge der Vermutung, dass sich diese Wahrscheinlichkeit für einen festgelegten Fehler auf den meisten zufälligen Eingaben mit polynomial vielen klassischen Abfragen annähern lässt.

Damit betrifft die Folgerung die Zahl der abgefragten Eingabebits unter bestimmten Bedingungen: betrachtet werden zufällige Eingaben sowie festgelegte Fehler- und Ausnahmeanteile. Sie ist keine allgemeine Aussage über die Gesamtlaufzeit beliebiger Quantenalgorithmen.

Am 6. November sagte PSI, Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan von der Stanford University läsen den Beweis, hätten Kommentare geschickt und arbeiteten an einer kürzeren Fachdarstellung.