OpenAI объявила, что её система искусственного интеллекта сгенерировала математические доказательства, которые, по заявлению компании, способны поставить под сомнение ряд устоявшихся представлений в математике и компьютерных науках. Центральным результатом стала работа над гипотезой локального сглаживания — задачей гармонического анализа, сформулированной математиком Кристофером Согге ещё в 1991 году. По словам разработчиков, модели OpenAI доказали эту гипотезу для всех пространственных измерений, а итоговое доказательство было сгенерировано 18 октября 2026 года и уже на следующий день формализовано в интерактивной среде Lean.
Что такое гипотеза локального сглаживания
Гипотеза описывает поведение волн в момент их концентрации и утверждает, что экстремальная фокусировка волнового поля не может поддерживаться длительное время. Формально речь идёт о оценке нормы оператора эволюции (в записи, приведённой в материалах компании, — через экспоненциальный оператор с квадратным корнем из лапласиана) в пространствах Лебега на многообразии M. До работы OpenAI учёные лишь приближались к полному результату: в 2019 году гипотеза сглаживания была доказана для двух измерений, а в 2025 году подтверждена трёхмерная гипотеза Кокеи. Новое доказательство, по заявлению разработчиков, автоматически закрывает ещё два известных математических вопроса, связанных с этой темой.
Как ИИ пришёл к решению и почему это важно
Согласно сообщению OpenAI, именно нейросетевые модели компании вывели доказательство, охватывающее все пространственные измерения, то есть обобщившее предыдущие частные случаи. Это позиционируется как прорыв, поскольку задача оставалась открытой более тридцати пяти лет и выходила за рамки стандартных вычислительных подходов. Компания подчёркивает, что результат может пересмотреть ряд устоявшихся представлений как в чистой математике, так и в смежных разделах компьютерных наук.
Формализация в Lean и открытая стратегия
Для обеспечения проверяемости OpenAI выбрала открытую стратегию: текстовые и формализованные доказательства опубликованы в открытом доступе на GitHub. Ключевым шагом стала формализация в Lean — специализированном инструменте, который позволяет компьютеру проверять логическую корректность математических аргументов. По данным компании, формализация была успешно завершена 19 октября 2026 года, на следующий день после генерации доказательства. Это означает, что независимый исследователь может воспроизвести и проверить каждый логический шаг с помощью компьютера, а не полагаться только на текстовое описание.
Квантовая хромодинамика и независимая проверка
Помимо математического результата, исследователи сообщили о доказательстве существования теорий, описывающих поведение материи на уровне мельчайших частиц, в частности квантовой хромодинамики. Исследования в области квантовой физики, по информации OpenAI, будет вести отдельная внешняя группа учёных, которая в ближайшее время подготовит собственный независимый аналитический отчёт. Таким образом, часть заявлений компании пока остаётся на стадии ожидания внешнего верификационного отчёта.
