# PSI заявила о доказательстве гипотезы Ааронсона — Амбайниса для квантовых систем

- Опубликовано: 2026-11-07 02:19 UTC
- Раздел: Цифра и вычисления › Квантовые технологии
- Теги: гипотеза Ааронсона — Амбайниса, квантовые алгоритмы, Lean, PSI, квантовое преимущество, теория алгоритмов
- Адрес: https://realtech.media/ru/news/rt-7a92aa8a6e3b4107e86b0c86_psi_zayavila_o/

**Компания PSI сообщила, что её исследовательская система за три дня нашла доказательство математической проблемы 2008 года с верификацией в Lean.**

![PSI claims formal proof of Aaronson-Ambainis quantum computing conjecture](https://realtech.media/media/2026/11/de25792af5237244.jpg)
*Anita Fors (Chalmers), Wikimedia Commons, CC BY-SA 4.0*

Исследовательская компания PSI заявила, что её система за три дня сформировала математическое доказательство гипотезы Ааронсона — Амбайниса, остававшейся нерешённой в течение 18 лет, сообщает Interesting Engineering [1]. Сформулированная в 2008 году проблема определяет условия, при которых квантовые вычислители получают экспоненциальное преимущество в скорости перед классическими архитектурами. Логическая корректность выкладок была проверена программным верификатором Lean, однако работа ещё не прошла полноценное академическое рецензирование [1].

## Проверка и границы квантового ускорения

По данным PSI, вычисления велись на собственной инфраструктуре с привлечением непубличной модели от Anthropic [1]. Система сгенерировала формальное математическое доказательство, которое успешно прошло проверку в интерактивной среде Lean. Разработчики отметили, что алгоритм дважды оптимизировал цепочку логических выводов, и итоговая версия аргументации также была подтверждена программным верификатором [1].

Гипотеза Ааронсона — Амбайниса описывает объём информации, требуемый классическому компьютеру для моделирования работы ряда квантовых алгоритмов. В случае справедливости гипотезы классические вычислители способны моделировать определённый класс квантовых процедур на случайных входных данных лишь с полиномиальными накладными расходами [1]. Это разграничение объясняет, почему квантовые алгоритмы определённой структуры не дают экспоненциального ускорения, хотя специализированные методы, такие как алгоритм Шора для факторизации чисел, под данные ограничения не подпадают [1].

## Участники работы и научный аудит

Разработку исследовательской системы, постановку задачи и запуск вычислений в PSI выполнил Дэвид Туртурян, который также провёл вычитку черновика [1]. Аудит доказательства выполнил Джим Халверсон, а Фиала Шанахан предоставила комментарии по формализации логики в среде Lean [1].

К анализу результатов подключилась группа исследователей из Стэнфордского университета, включая Гая Блана, Джордана Доктера, Кармен Страссл и Ли-Яна Тана, доказавших частный случай гипотезы в августе 2026 года [1]. Учёные готовят краткое изложение доказательства для академического сообщества: среде Lean доступна лишь сверка формальной непротиворечивости шагов, тогда как независимая экспертиза должна подтвердить эквивалентность формализованной теоремы исходной формулировке 2008 года [1].

## Источники

1. [Interesting Engineering](https://interestingengineering.com/culture/psi-research-system-aaronson-ambainis-quantum-conjecture)

---

Источник: RealTech, realtech.media — https://realtech.media/ru/news/rt-7a92aa8a6e3b4107e86b0c86_psi_zayavila_o/