Das US-Labor Physical Superintelligence (PSI) hat am 6. November einen Beweis der Aaronson-Ambainis-Vermutung veröffentlicht, zusammen mit einer Lean-4-Formalisierung, die jeder nachrechnen kann. Die Vermutung ist seit 2008 offen und zählt zu den zentralen Problemen der Quantenabfragekomplexität. Laut PSI stammt der Beweis von einem intern gebauten Forschungssystem, das Instanzen eines nicht öffentlichen Anthropic-Modells ausführte: Am dritten Tag des Laufs lag ein vollständiger Beweis vor, Lean akzeptierte ihn, danach wurde das System auf verwandte offene Probleme angesetzt und verbesserte das Ergebnis zweimal.
Was die Vermutung aussagt
Shors Algorithmus faktorisiert schnell, weil die Eingabe ein wiederkehrendes Muster verbirgt. Aaronson und Ambainis stellten die härtere Frage: Kann ein Quantencomputer bei zufälligen Eingaben exponentiell schneller sein, wo es keine solche Struktur gibt? Sie reduzierten das auf reine Mathematik. Nach T Abfragen ist die Annahmewahrscheinlichkeit eines Quantenalgorithmus ein Polynom in den Eingabebits vom Grad höchstens 2T mit Werten in [0,1]. Hat ein solches Polynom stets eine einflussreiche Variable — ein Bit, dessen Kippen den Wert nicht vernachlässigbar verändert —, kann eine klassische Maschine den Quantencomputer mit polynomiell vielen Abfragen nachahmen. Bei Ja/Nein-Fragen über zufällige Zeichenketten gibt es keinen exponentiellen Quantenvorteil.
PSIs neue Ungleichung: Für ein Polynom f vom Grad d, beschränkt auf [0,1], mit Varianz v, gilt für ein Bit i: Inf_i(f) ≥ c·v^(5/2)/d^6 ≥ (v/d)^7 mit c = 8√15/(125π⁴) ≈ 0,0025. Frühere allgemeine Schranken fielen exponentiell mit dem Grad ab — genau deshalb blieb die Frage offen. Der Beweis folgt einem Plan von Shachar Lovett und Jiapeng Zhang und ersetzt deren einzige vermutete Ungleichung durch eine neue, die durch eine Eins-zu-eins-Paarung von Schaltereinstellungen über eine Determinante bewiesen wird; David Reimers Schmetterlingslemma liefert eine schwächere Paarung.
Was man selbst prüfen kann
Die Formalisierung ist öffentlich und auf Lean 4.33.0 sowie Mathlib v4.33.0 festgelegt. `make check` führt eine Importprüfung, ein statisches Audit (kein `sorry`, `axiom` oder `native_decide` in der Bibliothek), den Build und einen Axiombericht aus: Die vier abschließenden Theoreme stützen sich nur auf propext, Classical.choice und Quot.sound. `make replay` prüft den Kernel mit leanchecker erneut — das README nennt rund 7,4 GB und 11 Minuten auf einem Thread —, zusätzlich werden ein zweiter Kernel (lean4lean) und ein Comparator-Lauf berichtet. Das Repository stand bei den ersten Analysen bei einem Commit und sechs Sternen; Lizenz: Apache 2.0.
Was Lean nicht prüfen kann
- **Treue der Aussage.** Ob die Lean-Aussage `PrintedConjecture` der gedruckten Vermutung entspricht, bleibt laut README einem menschlichen Leser überlassen. Ein gültiger Beweis einer subtil schwächeren Aussage beweist das Falsche. - **Eine nicht formalisierte Voraussetzung.** Die Hypothese `FbsDegreeBound` von Agarwal und Ben-David ist Eingabe eines Theorems und selbst nicht formalisiert. - **Das Paper.** Das Manuskript ist nicht maschinengeprüft. Es wurde vom Modell entworfen und von der Person überprüft, die das System betrieb. - **Begutachtung.** Es gibt keine. Jim Halverson prüfte den Beweis intern, Phiala Shanahan kommentierte die Formalisierung. - **Reproduzierbarkeit des Laufs.** Das Modell ist nicht öffentlich; prüfbar ist nur das Ergebnis, nie der Prozess.
Weder Scott Aaronson noch Andris Ambainis haben sich öffentlich geäußert. Vier Stanford-Forscher — Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan, die im August einen Spezialfall für Algorithmen mit fester Zahl paralleler Runden bewiesen — werden auf PSIs Seite mit den Worten zitiert, es sei ein „enormes Ergebnis“, dessen Beweis mehrere Arbeitslinien „auf recht magische Weise“ zusammenführe. Die Zitate gibt PSI weiter; die Forscher selbst haben sie nicht veröffentlicht.
Warum das über den Satz hinaus zählt
Es ist die dritte PSI-Veröffentlichung binnen eines Monats im selben Zuschnitt: ein formales Artefakt, das jeder prüfen kann, um eine Behauptung gelegt, die von außen noch niemand genau gelesen hat. Dieser Zuschnitt wird zur Vorlage, und für Entwickler ist er eine gute: Toolchain festnageln, Axiome auditieren, ein Replay-Ziel liefern und ausdrücklich auflisten, was nicht geprüft ist. Die verbleibende Lücke ist nicht technisch. Es sind die Wochen fachlicher Lektüre, die zeigen müssen, dass die formale Aussage das Problem ist, das Menschen interessiert.
Drei Signale werden das klären: eine öffentliche Einschätzung von Aaronson oder Ambainis, die kürzere Darstellung, die die Stanford-Gruppe laut PSI schreibt, und eine arXiv- oder Zeitschrifteneinreichung. Bis dahin lautet die ehrliche Beschreibung: ein maschinengeprüfter Beweis einer Aussage, die noch einen Menschen braucht, um sie mit der Vermutung zu verbinden.
