ИИ за три дня нашёл доказательство математической гипотезы, которую не могли решить 18 лет

Американская исследовательская компания Physical Superintelligence (PSI) объявила о решении математической задачи, остававшейся открытой с 2008 года. Система искусственного интеллекта, использующая экспериментальную модель Anthropic, за три дня нашла доказательство гипотезы Ааронсона — Амбайниса, связанной с возможностями квантовых компьютеров. Доказательство прошло автоматическую проверку в математической системе Lean, однако его независимая научная экспертиза ещё продолжается.

Гипотезу предложили американский учёный Скотт Ааронсон и латвийский математик Андрис Амбайнис. Она касается одного из фундаментальных вопросов квантовых вычислений: при каких условиях квантовый компьютер способен решать задачи экспоненциально быстрее обычного. Такое ускорение означает, что по мере увеличения размера задачи разница в необходимых вычислительных ресурсах может становиться огромной.

Квантовые компьютеры используют суперпозицию и другие квантовые эффекты для обработки информации. Благодаря этому некоторые алгоритмы способны значительно сокращать количество операций, необходимых для получения результата. Например, алгоритм Шора позволяет находить простые множители больших чисел значительно эффективнее известных классических методов. Однако подобные преимущества обычно связаны с определённой математической структурой задачи.

Ааронсон и Амбайнис предположили, что для случайных входных данных, не обладающих такой структурой, возможности квантового ускорения существенно ограничены. Их гипотеза связывала этот вопрос со свойствами математических многочленов, описывающих вероятность определённого результата квантового вычисления. Если предположение верно, обычный компьютер может приблизительно воспроизводить результаты определённых квантовых алгоритмов, обращаясь к входным данным лишь в полиномиально большее число раз.

За прошедшие 18 лет математикам удалось доказать несколько частных случаев гипотезы, однако общее решение оставалось неизвестным. В августе 2026 года исследователи Стэнфордского университета получили важный результат для квантовых алгоритмов, использующих фиксированное число параллельных обращений к входным данным. Новая работа PSI претендует на доказательство первоначальной гипотезы без этого ограничения.

Для поиска решения компания использовала собственную исследовательскую систему, созданную под руководством Дэвида Туртуряна. В её работе участвовали экземпляры ещё не выпущенной публично модели Anthropic. Искусственный интеллект анализировал существующие математические результаты, предлагал новые подходы и проверял промежуточные рассуждения. Уже на третий день система получила полное доказательство, которое было принято программой Lean.

Lean предназначена для формальной проверки математических доказательств. В отличие от обычной языковой модели, способной сформулировать убедительное, но ошибочное рассуждение, такая система проверяет логическую последовательность математических утверждений в соответствии с заданными правилами. Это позволяет обнаруживать ошибки, которые могут остаться незамеченными при традиционной проверке большого количества сложных выкладок.

После получения первого результата исследовательская система дважды улучшила доказательство. Окончательная версия устанавливает конкретную математическую границу, показывающую, что у многочлена небольшой степени, значения которого находятся между нулём и единицей, обязательно существует переменная с достаточно большим влиянием на результат. Именно такое свойство было необходимо для доказательства гипотезы. Все версии прошли формальную проверку Lean.

Согласно полученному результату, для широкого класса задач с равномерно случайными входными данными классический компьютер может приблизительно оценить вероятность ответа квантового алгоритма без экспоненциального увеличения числа обращений к данным. При этом доказательство касается количества таких обращений, а не общего времени вычислений. Оно также не исключает существенных преимуществ квантовых компьютеров при решении специально структурированных задач, включая разложение больших чисел на множители.

Проверка Lean охватывает основную математическую теорему, но не все выводы и пояснения статьи. Работа пока не опубликована в рецензируемом научном журнале, а независимая проверка соответствия формальных утверждений исходной гипотезе ещё не завершена.

Дэвид Туртурян лично определил исследовательскую задачу, организовал работу системы и проверил подготовленную рукопись. Математик Джим Халверсон провёл дополнительную проверку доказательства, а физик Фиала Шанахан изучила его формальное представление в Lean. Исследователи Гай Блан, Джордан Доктер, Кармен Страссле и Ли-Ян Тан, ранее доказавшие частный случай гипотезы, также изучают новую работу и готовят сокращённое изложение доказательства для математического сообщества.