Перейти к содержимому

Математический прорыв OpenAI оказался под угрозой: учёные обнаружили расхождения в доказательстве задачи на миллион долларов

Громкое заявление OpenAI о решении одной из самых сложных математических задач в мире столкнулось с новыми вопросами. Исследователи обнаружили расхождения между текстовым объяснением доказательства и его формальной версией на языке Lean. Теперь учёным предстоит выяснить, действительно ли искусственный интеллект решил задачу тысячелетия или в представленном результате есть ошибки.


Основная новость

В начале сентября 2026 года OpenAI объявила о математическом прорыве: внутренняя модель компании, работавшая совместно с множеством ИИ-агентов, представила решение проблемы существования и гладкости уравнений Навье — Стокса. Эта задача десятилетиями оставалась одной из наиболее известных нерешённых проблем современной математики.

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

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

Что именно обнаружили исследователи

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

Но автоматическая проверка имеет важное ограничение: компьютер проверяет именно ту формальную конструкцию, которая ему передана. Он не может автоматически гарантировать, что эта конструкция полностью соответствует первоначальному объяснению исследователя.

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

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

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

Почему задача Навье — Стокса так важна

Уравнения Навье — Стокса описывают движение жидкостей и газов. Они используются в аэродинамике, гидродинамике, метеорологии и инженерных расчётах.

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

За решение этой задачи Математический институт Клэя назначил премию в размере одного миллиона долларов. Она входит в список семи задач тысячелетия — фундаментальных математических проблем, сформулированных в 2000 году.

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

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

Почему искусственный интеллект пока нельзя считать окончательным арбитром

Современные ИИ-системы способны генерировать сложные математические рассуждения, писать код и формализовать доказательства. Но переход от идеи к формально проверяемой записи остаётся отдельной задачей, на которой возможны ошибки.

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

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

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

Что будет дальше

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

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

Вывод

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

Пока нет комментариевВойдите в аккаунт, чтобы начать обсуждение.