9 сентября 2026 г.
Решение задачи Навье — Стокса можно проверить: OpenAI опубликовала доказательство в Lean
OpenAI заявила о решении одной из «Задач тысячелетия» и выложила доказательство вместе с кодом проверки.
По данным OpenAI, 5 сентября группа из 10 тысяч ИИ-агентов нашла решение за 88 часов. Формализация и проверка в Lean заняли ещё 17 часов.
Уравнения Навье — Стокса описывают движение жидкостей и газов. Ими пользуются при проектировании самолётов и прогнозировании погоды. Задача состояла в том, чтобы выяснить, всегда ли изначально гладкое течение остаётся гладким.
OpenAI опубликовала доказательство на 166 страницах: при любой положительной вязкости можно построить трёхмерное течение с гладкой внешней силой, в котором скорость становится неограниченной за конечное время. Кинетическая энергия при этом остаётся ограниченной. Речь о поведении математического решения. [Доказательство OpenAI](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf).
Как участвовал Codex. Исследователи поручали ему объединять полезные промежуточные результаты разных групп агентов. Из этих результатов составляли следующие промпты, включая задания для группы, нашедшей решение. Поиск вела внутренняя модель, которую OpenAI называет существенно сильнее GPT-6 Astra, а Astra использовали для формализации и проверки.
На задачу Навье — Стокса ушло 130 млрд выходных токенов и 2,7 млн сообщений агентов. Это часть общего эксперимента с несколькими математическими задачами, на который OpenAI потратила 300 млрд токенов. [Описание эксперимента OpenAI от 8 сентября](https://openai.com/index/navier-stokes-solution/).
Что доступно практику. OpenAI выложила формализацию в репозиторий NavierStokesAndEuler. Lean проверяет доказательство, записанное на формальном языке. Для сборки нужны elan и зависимости проекта, включая Lean 4.34.0-rc2. Из корня репозитория выполняются команды:
```sh lake exe cache get lake build ```
Для независимой проверки через Comparator нужны `landrun`, `lean4export` и `nanoda_bin` в PATH. После загрузки кэша запускается `lake exe comparator ComparatorChallenges/NavierStokes.json`. [Репозиторий и инструкции проверки](https://github.com/openai/NavierStokesAndEuler).
В параллельной работе математики Тристан Бакмастер и Левент Альпёге использовали Claude и Codex, особенно GPT-5.6 Sol. Результат для уравнений Эйлера они получили 15 августа и проверили в Lean 22 августа. В сентябрьском эксперименте OpenAI исследователи уже поручили группам агентов самостоятельный поиск решения.
Модель, которая вела поиск доказательства OpenAI, остаётся внутренней и недоступна публике.
Первоисточник
