Система PSI заявила про доведення гіпотези Ааронсона-Амбайніса

07 листопада 2026 р. 11:25

07 листопада 2026 р. 11:25

Американська компанія PSI, що працює у сфері фізики, повідомила, що її автоматизована дослідницька система за три дні побудувала формальне доведення гіпотези Ааронсона-Амбайніса. Ця задача про межі квантових обчислень залишалася відкритою близько 18 років. Про результати команда розповіла в матеріалі видання Interesting Engineering .

За даними PSI, система використала непублічну модель від Anthropic, запущену на власній інфраструктурі компанії. Вона згенерувала математичне доведення, яке потім було перевірене програмою Lean — спеціальним «асистентом доведень», що формально перевіряє логічну коректність математичних аргументів.

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

Про що гіпотеза Ааронсона-Амбайніса

Гіпотеза Ааронсона-Амбайніса, сформульована у 2008 році, стосується того, скільки інформації потрібен класичному комп’ютеру, щоб імітувати певні квантові алгоритми. Більш конкретно, йдеться про те, чи можуть квантові алгоритми з певною математичною структурою бути ефективно апроксимовані класичними методами.

Якщо гіпотеза правильна, то класичні комп’ютери здатні імітувати широкий клас таких квантових алгоритмів для випадково обраних вхідних даних з лише поліноміальними накладними витратами. Різниця між поліноміальним і експоненціальним зростанням критична: зі збільшенням розміру задачі обчислювальні вимоги в цих двох випадках відрізняються на порядки.

Це, за задумом авторів гіпотези, допомагає пояснити, чому деякі квантові алгоритми можуть не давати очікуваної експоненціальної переваги над класичними, навіть якщо сама квантова апаратура оперує зовсім іншими, ніж у класичної електроніки, принципами обробки інформації.

Разом з тим можливе доведення гіпотези не заперечує існування задач, де квантові комп’ютери мають істотну перевагу. Наприклад, алгоритм Шора для факторизації великих чисел гіпотезою не спростовується. Вона стосується конкретного класу квантових обчислень і умов, за яких їхня видима перевага може бути відтворена класичними засобами.

Як перевіряли доведення

PSI повідомляє, що роботою керував Девід Туртуреан (David Turturean): він розробив дослідницьку систему, сформулював задачу для неї та запускав процес. Також він редагував отриманий проєкт статті й відповідав за правильність викладеного доведення.

За даними компанії, Джим Гелверсон (Jim Halverson) перевіряв доведення, а Фіала Шенеган (Phiala Shanahan) коментувала його формалізацію в Lean. Окрему увагу приділили саме формальній перевірці: Lean здатен упевнитися, що всі кроки строго випливають з припущень, однак цього недостатньо, щоб вважати математичну проблему остаточно розв’язаною.

Формальний асистент доведень перевіряє логіку, але не зміст. Тому дослідникам ще належить з’ясувати, чи точно формально записана задача в Lean збігається з початковим формулюванням гіпотези Ааронсона-Амбайніса.

Роль незалежних математиків

До аналізу роботи PSI вже долучилися науковці зі Стенфордського університету. Серед них називають Гая Бланка (Guy Blanc), Джордана Доктера (Jordan Docter), Кармен Страссле (Carmen Strassle) та Лі-Янга Тана (Li-Yang Tan). Ця група ще в серпні 2026 року довела окремий, спеціальний випадок гіпотези й зараз готує коротший виклад повного доведення PSI для інших фахівців.

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

PSI, що публічно стартувала у вересні 2026 року, позиціонує себе як фізичну дослідницьку компанію, яка будує автоматизовані системи для наукових відкриттів. Поточна заява про розв’язання гіпотези Ааронсона-Амбайніса може стати важливою віхою як для квантової теорії обчислень, так і для використання штучного інтелекту в математиці. Проте результат ще має витримати широку перевірку експертів, перш ніж його можна буде вважати усталеним науковим фактом.

Наука