AI przygotowała dowód ważnej hipotezy o przewadze komputerów kwantowych

System badawczy firmy Physical Superintelligence (PSI) znalazł dowód hipotezy Aaronsona-Ambainisa, otwartego od 2008 roku problemu z pogranicza teorii obliczeń kwantowych i klasycznych. Wynik nie jest jednak historią o maszynie, która sama zastąpiła matematyków. Najważniejszym elementem jest formalizacja w Lean, gdzie każdy krok dowodu może sprawdzić komputer.

PSI opisało projekt na swojej stronie, a David Turturean opublikował 6 listopada 2026 roku preprint na arXiv. Zgodnie z dokumentacją projektu system korzystał z niepublicznych instancji modelu Anthropic, działając w wewnętrznym środowisku badawczym. Według PSI pełny dowód powstał trzeciego dnia pracy, po czym Lean zaakceptował jego formalną wersję.

Co właściwie udowodniono?

Hipoteza dotyczy funkcji opisujących problemy na n-bitowych danych. W uproszczeniu pyta, czy wielomian o niskim stopniu, którego wartości pozostają ograniczone, musi mieć przynajmniej jedną zmienną o wyraźnym wpływie na wynik. Aaronson i Andris Ambainis wysunęli tę hipotezę, ponieważ jej spełnienie ograniczałoby skalę przewagi algorytmów kwantowych w modelu zapytań.

W opublikowanym wyniku dla wielomianu stopnia co najwyżej d i wariancji co najmniej ε wskazano zmienną, której wpływ jest ograniczony od dołu wyrażeniem proporcjonalnym do ε^5/2/d⁶. To rezultat teoretyczny, ale jego znaczenie jest konkretne: sugeruje, że nadzwyczajne, superwielomianowe przyspieszenia kwantowe wymagają dodatkowej struktury problemu, na przykład obietnicy dotyczącej danych wejściowych.

Lean zmienia wagę deklaracji

Sam tekst dowodu wygenerowany przez model nie byłby wystarczającym powodem, by uznać hipotezę za rozstrzygniętą. W repozytorium PSI znajduje się artykuł, kod Lean oraz opis kontroli założeń. Autorzy deklarują, że formalizacja nie korzysta z luk ani dodatkowych aksjomatów, a jądro Lean sprawdziło cztery główne twierdzenia. To nie zastępuje niezależnej oceny ekspertów, ale znacząco ogranicza ryzyko zwykłego błędu rachunkowego lub logicznego.

Warto też zachować proporcje. Preprint i formalizacja są publiczne, lecz wynik dopiero trafia do szerszej kontroli środowiska matematycznego. Formalny certyfikat potwierdza zgodność dowodu z przyjętymi definicjami i regułami systemu; nie odpowiada samodzielnie na pytania o czytelność argumentu, wybór modelu ani znaczenie dla wszystkich rodzajów komputerów kwantowych.

Dlaczego to ważne dla AI?

Przypadek PSI pokazuje model pracy, w którym model językowy jest częścią większego laboratorium: dostaje narzędzia, pamięć, środowisko symulacyjne i możliwość sprawdzania hipotez. Człowiek nadal ustala problem, ocenia sens rozwiązania i musi umieć wyjaśnić wynik innym badaczom. W matematyce można dodatkowo zamknąć pętlę weryfikacji w kodzie. W fizyce eksperymentalnej taki krok jest trudniejszy, bo obliczenia trzeba jeszcze skonfrontować z naturą.

Dlatego ten wynik jest zarówno osiągnięciem matematycznym, jak i testem nowego modelu prowadzenia badań. Jeśli podobne systemy będą regularnie tworzyć sprawdzalne dowody, największą zmianą może okazać się nie sam fakt użycia AI, lecz skrócenie drogi od pytania do wiarygodnego, reprodukowalnego wyniku.

Źródła

• Physical Superintelligence: A proof of the Aaronson-Ambainis conjecture
• David Turturean, A proof of the Aaronson-Ambainis conjecture, arXiv
• Repozytorium PSI z formalizacją Lean
• Scott Aaronson i Andris Ambainis, The Need for Structure in Quantum Speedups