PSI (Physical Superintelligence) заявила, що її дослідницька система на неопублікованій моделі Anthropic знайшла доказ гіпотези Aaronson-Ambainis, відкритої з 2008 року. Lean прийняв доказ.

Що стверджує гіпотеза Aaronson-Ambainis?

Гіпотеза стверджує: якщо значення полінома, що лежить між 0 і 1, змінюється між входами, то існує біт, перемикання якого змінює це значення в середньому щонайменше на фіксований степінь дисперсії, за даними PSI. Такий поліном описує ймовірність відповіді «так» квантового алгоритму, а його складність обмежена кількістю запитів алгоритму до входу.

Класичний алгоритм у цій схемі знає поліном квантового. Він послідовно зчитує біт із великим впливом, а коли решта бітів майже не змінює відповідь, зупиняється й видає середнє значення. Гіпотеза гарантує, що до зупинки завжди лишається такий біт.

Наслідок: для питань «так/ні» на рівномірно випадкових входах існує детермінований класичний алгоритм, який наближає ймовірність відповіді «так» квантового алгоритму на всіх входах, крім малої частки. Кількість класичних запитів зростає як фіксований степінь кількості квантових, а не експоненційно, за даними The Quantum Insider.

Контекст: алгоритм Peter Shor 1994 року розкладає великі числа на множники швидше за відомі класичні методи, бо задача приховує повторюваний візерунок. Питання було в тому, чи можливе експоненційне прискорення на випадковому рядку нулів і одиниць без такої структури.

Чого ця теорема не стверджує?

Теорема обмежує кількість звернень до входу, а не повний час обчислень, тому вона не є загальною межею для квантових машин і не визначає їхньої комерційної цінності. Результат вужчий і з інших причин: він стосується лише питань «так/ні» і лише більшості випадкових входів.

Практичний висновок для розробників квантових алгоритмів: перевагу варто шукати в задачах, чия математична чи фізична структура її дає, як періодичність у Shor. Теорема підсилює теоретичне обґрунтування цього підходу, але не вказує, які застосунки справді виграють.

Що відомо про перевірку доказу і роль AI?

PSI стверджує, що система мала повний доказ на третій день запуску на власній інфраструктурі, а Lean, де комп'ютер перевіряє кожен крок, його прийняв. Потім систему спрямували на суміжні відкриті задачі: вона двічі покращила результат, і Lean прийняв фінальну версію.

Межі перевірки такі. За статтею David Turturean з PSI, у Lean формалізовано головну теорему та формулювання оригінальної гіпотези, а ядро Lean перевірило логічні кроки. Lean гарантує коректність кроків, але чи точно формалізація передає гіпотезу, оцінюють люди. У джерелах про це згадано лише читання доказу авторами зі Stanford. Про незалежну рецензію вони не повідомляють.

Guy Blanc, Jordan Docter, Carmen Strassle і Li-Yang Tan зі Stanford у серпні 2026 року довели окремий випадок: відсутність експоненційного прискорення для квантових алгоритмів, що читають вхід у фіксованій кількості паралельних раундів. Тепер вони читають доказ повної гіпотези, надсилають PSI коментарі й готують коротший виклад для фахівців. Вони написали PSI: «Це величезний результат. Він розв'язує гіпотезу, якій десятиліття, і має важливі наслідки для розуміння задач, що допускають квантове прискорення».

Для оцінки AI-систем це важливий приклад: твердження про доказ можна перевіряти формально, а не лише довіряти розробникові. Але швидкість (третій день запуску) і внесок моделі тут відомі лише зі слів PSI.