Как сообщили представители PSI, в исследовательской системе они использовали непубличную модель Anthropic, работающую на собственной инфраструктуре PSI. Система подготовила математическое доказательство, которое было принято программой Lean — инструментом для автоматизированной проверки логической корректности формальных математических доказательств. Впоследствии система дважды усовершенствовала доказательство, и финальная версия также была одобрена Lean. Тем не менее, независимая академическая экспертиза еще впереди, пишет Quantum Insider.
Гипотеза Ааронсона — Амбайниса отвечает на вопрос, какой объем информации необходим классическому компьютеру для имитации определенных квантовых алгоритмов. Если точнее, речь идет о том, можно ли эффективно аппроксимировать с помощью классических компьютеров квантовые алгоритмы, обладающие определенной математической структурой. Если эта гипотеза верна, то классические компьютеры могли бы имитировать широкий класс квантовых алгоритмов для случайно выбранных входных данных, при этом вычислительные затраты возросли бы лишь полиномиально. Различие принципиальное: при увеличении размера задачи полиномиальный и экспоненциальный рост приводят к совершенно разным требованиям к вычислительным ресурсам.
Если гипотеза верна, она объясняет, почему некоторые квантовые алгоритмы могут не обеспечивать экспоненциального преимущества перед классическими вычислительными методами — даже несмотря на то, что квантовое оборудование способно обрабатывать информацию принципиально иными способами.
Компания PSI, публично заявившая о себе в сентябре 2026 года, позиционирует себя как исследовательская организация в области физики, создающая автоматизированные системы для научных открытий.
В начале осени компания Anthropic с помощью своей языковой модели Claude впервые в истории перевела в компьютерно-верифицируемый код доказательство великой теоремы Ферма — одной из самых сложных математических задач XX века. За 11 дней ИИ превратил работу Эндрю Уайлса и Ричарда Тейлора в 13-миллионнострочное формальное доказательство на языке Lean, на что у людей ушло бы около 10 лет.
