PSI заявила о доказательстве гипотезы Ааронсона — Амбайниса для квантовых систем
Компания PSI сообщила, что её исследовательская система за три дня нашла доказательство математической проблемы 2008 года с верификацией в Lean.
Исследовательская компания PSI заявила, что её система за три дня сформировала математическое доказательство гипотезы Ааронсона — Амбайниса, остававшейся нерешённой в течение 18 лет, сообщает Interesting Engineering interestingengineering.com
Interesting Engineeringinterestingengineering.comОткрыть источник ↗. Сформулированная в 2008 году проблема определяет условия, при которых квантовые вычислители получают экспоненциальное преимущество в скорости перед классическими архитектурами. Логическая корректность выкладок была проверена программным верификатором Lean, однако работа ещё не прошла полноценное академическое рецензирование.
Проверка и границы квантового ускорения
По данным PSI, вычисления велись на собственной инфраструктуре с привлечением непубличной модели от Anthropic. Система сгенерировала формальное математическое доказательство, которое успешно прошло проверку в интерактивной среде Lean. Разработчики отметили, что алгоритм дважды оптимизировал цепочку логических выводов, и итоговая версия аргументации также была подтверждена программным верификатором.
Гипотеза Ааронсона — Амбайниса описывает объём информации, требуемый классическому компьютеру для моделирования работы ряда квантовых алгоритмов. В случае справедливости гипотезы классические вычислители способны моделировать определённый класс квантовых процедур на случайных входных данных лишь с полиномиальными накладными расходами. Это разграничение объясняет, почему квантовые алгоритмы определённой структуры не дают экспоненциального ускорения, хотя специализированные методы, такие как алгоритм Шора для факторизации чисел, под данные ограничения не подпадают.
Участники работы и научный аудит
Разработку исследовательской системы, постановку задачи и запуск вычислений в PSI выполнил Дэвид Туртурян, который также провёл вычитку черновика interestingengineering.com
Interesting Engineeringinterestingengineering.comОткрыть источник ↗. Аудит доказательства выполнил Джим Халверсон, а Фиала Шанахан предоставила комментарии по формализации логики в среде Lean.
К анализу результатов подключилась группа исследователей из Стэнфордского университета, включая Гая Блана, Джордана Доктера, Кармен Страссл и Ли-Яна Тана, доказавших частный случай гипотезы в августе 2026 года. Учёные готовят краткое изложение доказательства для академического сообщества: среде Lean доступна лишь сверка формальной непротиворечивости шагов, тогда как независимая экспертиза должна подтвердить эквивалентность формализованной теоремы исходной формулировке 2008 года.
