6 listopada 2026 r. Physical Superintelligence (PSI) ogłosiła, że jej wewnętrzny system, korzystający z niepublicznego modelu Anthropic, uzyskał dowód hipotezy Aaronsona–Ambainisa, a formalizację zaakceptował Lean. Hipoteza dotyczy wpływu pojedynczych bitów na ograniczone wielomiany; rozstrzygnięcie tego problemu miałoby znaczenie dla analizy zapytań kwantowych. PSI opisała swoje twierdzenie i jego kontekst.
Publiczne repozytorium PSI podaje dokładne warunki formalnego twierdzenia. Zaznacza też, że samo sprawdzenie w Lean nie potwierdza, czy zapisane twierdzenie odpowiada zamierzonej treści hipotezy.
Sprawdzenie dowodu przez Lean potwierdza jego zgodność z formalnie zapisanym twierdzeniem; interpretacja tego twierdzenia pozostaje osobnym krokiem.
Jakie twierdzenie zapisano w repozytorium PSI
Formalizacja dotyczy wielomianu rzeczywistego stopnia co najwyżej d, który przyjmuje wartości od 0 do 1 na zbiorze wejść binarnych {0,1}^N. Jego wariancja przy równomiernym rozkładzie wejść musi wynosić co najmniej ε, gdzie ε > 0. Przy tych założeniach co najmniej jedna współrzędna ma wpływ na wartość wielomianu przekraczający wskazaną granicę.
Wpływ współrzędnej i to średnia wartość kwadratu zmiany wielomianu po odwróceniu bitu i. Repozytorium podaje dwie dolne granice tego wpływu: (8√15/(125π⁴)) · ε^(5/2)/d⁶ oraz (ε/d)^7. Własności twierdzenia i warunki formalizacji opisano w publicznym repozytorium PSI.
Repozytorium wiąże deklarację PrintedConjecture z hipotezą Aaronsona–Ambainisa w normalizacji przyjętej przez PSI. Jednocześnie pozostawia czytelnikom ustalenie, czy ta formalna definicja rzeczywiście wyraża zamierzoną treść hipotezy.
Co sprawdza Lean, a co pozostaje poza kontrolą
Lean to asystent dowodzenia: sprawdza, czy formalny dowód wynika z zapisanych twierdzeń i reguł systemu. Repozytorium PSI wymienia cztery końcowe deklaracje twierdzeń i informuje, że formalizacja nie zawiera luk ani dodanych aksjomatów. Opisuje też ponowne sprawdzenie deklaracji z użyciem kernela Lean oraz lean4lean, narzędzia do kontroli dowodów Lean.
Taka kontrola dotyczy formalnego zapisu. Repozytorium nie przedstawia jej jako sprawdzenia, czy PrintedConjecture jest właściwym sformułowaniem hipotezy Aaronsona–Ambainisa, ani jako maszynowej kontroli całego artykułu napisanego dla ludzi. W granicach zaufania wymienia również kernel i kompilator Lean, definicje z biblioteki Mathlib oraz maszyny wykonujące sprawdzenia.
PSI podała 6 listopada, że Guy Blanc, Jordan Docter, Carmen Strassle i Li-Yang Tan z Uniwersytetu Stanforda czytali dowód, przesłali uwagi i przygotowywali krótsze omówienie dla specjalistów. To opis etapu prac przekazany przez PSI w dniu ogłoszenia.
Jakie znaczenie ma wynik dla zapytań kwantowych
PSI wyjaśnia konsekwencję w modelu złożoności zapytań. Jeśli algorytm kwantowy wykonuje T zapytań, prawdopodobieństwo odpowiedzi „tak” można przedstawić jako ograniczony wielomian stopnia co najwyżej 2T. Według PSI twierdzenie pozwala wówczas przybliżyć to prawdopodobieństwo za pomocą klasycznych odczytów wejścia, których liczba rośnie wielomianowo, dla większości losowych wejść i przy ustalonym błędzie oraz odsetku wyjątków. Opis konsekwencji opublikowany przez PSI odnosi się do liczby zapytań, a nie do całkowitego czasu działania dowolnego algorytmu kwantowego ani wszystkich zadań obliczeniowych.
