OpenAI заявила о решении задачи Навье — Стокса и опубликовала формализацию в Lean

Компания представила не численный эксперимент, а конструкцию сингулярности

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

В формулировке Clay Mathematics Institute это отрицательный ответ на вопрос о безусловной глобальной гладкости. OpenAI пишет, что конструкция устанавливает варианты C и D официальной постановки Millennium Prize Problem. Важно различать заявление автора и окончательный математический статус: публикация рукописи и машинно проверяемого кода делает аргумент доступным для аудита, но сама по себе не заменяет независимое чтение, проверку предпосылок и процедуру признания результата.

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

Большие члены уравнения должны сократиться с высокой точностью

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

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

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

Поиск начался с параллельных ветвей доказательства и опровержения

Для задачи Навье — Стокса OpenAI запускала отдельные группы агентов на варианты A и B, ведущие к доказательству глобальной регулярности, и на варианты C и D, ведущие к контрпримеру. Группа, которая получила заявленный итог, включала порядка 10 000 одновременно работающих агентов. Компания сообщает, что вычисления проходили с мониторингом и изоляцией, применяемыми к оценке frontier-моделей.

Перед основной конструкцией система исследовала родственную задачу для уравнений Эйлера, то есть предел без вязкостного члена. Почти сто агентов примерно за 50 часов получили заявленное опровержение регулярности для невынужденного варианта Euler equations. После этого OpenAI перераспределила ресурсы с других Millennium Problems на Навье — Стокса и передала агентам найденную Euler-конструкцию как отправную точку.

По хронологии OpenAI первые агенты были запущены после 1 сентября, а решение появилось 5 сентября примерно через 88 часов. Формализация и проверка в Lean заняли ещё 17 часов с GPT‑6 Astra. Для самой задачи Навье — Стокса компания насчитала 2,7 миллиона сообщений агентов и около 130 миллиардов выходных токенов; по всем предпринятым задачам — 4,9 миллиона сообщений и примерно 300 миллиардов токенов.

Lean проверяет формальную цепочку, но не выбирает постановку за исследователя

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

Но машинная проверка отвечает на строго ограниченный вопрос: корректен ли формальный объект внутри выбранной библиотеки и спецификации. Независимым экспертам всё равно нужно сопоставить Lean-утверждение с официальной задачей Clay, проверить адекватность определений слабого и гладкого решения, свойства силы, начальных данных и энергии, а также убедиться, что бумажное объяснение не обещает больше формального theorem statement.

Поэтому практический критерий достоверности здесь двухслойный. Первый слой — воспроизводимая компиляция открытой формализации без доверия к внутренней инфраструктуре OpenAI. Второй — математическое рецензирование самой модели сингулярности и соответствия официальной постановке. До завершения такого аудита корректная формулировка новости — «OpenAI заявила и опубликовала доказательство», а не безусловное «задача окончательно закрыта».

Открытые материалы превращают громкое заявление в проверяемую гипотезу

Задача восходит к работам Клода-Луи Навье и Джорджа Габриэля Стокса XIX века. В 1934 году Жан Лере доказал существование обобщённых решений, но вопрос сохранения гладкости в трёх измерениях остался открытым. В 2000 году Clay Mathematics Institute включил его в семь Millennium Prize Problems.

Для исследований AI важен не только потенциальный математический результат, но и устройство процесса. Масштабная multi-agent система сначала нашла родственный механизм в Euler equations, затем перенесла его в более трудную вязкую постановку, после чего отдельная модель перевела рассуждение в формальный язык. Это заявленный пример связки массового поиска, аналитического синтеза и proof-assistant verification, а не обычный одиночный ответ чат-модели.

Следующий этап теперь находится вне внутреннего контура OpenAI: специалисты по PDE и формальной математике могут изучить рукопись, собрать Lean-код, сравнить theorem statements и попытаться найти контрпример к отдельным леммам. Даже если проверка выявит поправимые или фатальные проблемы, открытая публикация оставляет конкретный объект для анализа. Если же все уровни выдержат независимый аудит, работа станет одновременно результатом по одной из крупнейших задач анализа и демонстрацией нового масштаба автоматизированного математического поиска.