ИИ-агенты предложили решение задачи тысячелетия: OpenAI выложила доказательство Навье — Стокса

Математики около 90 лет выясняли, может ли изначально гладкое движение жидкости потерять гладкость за конечное время. OpenAI заявляет такой случай для трёхмерных уравнений Навье — Стокса с гладкой внешней силой. Жидкость первоначально покоится, а её кинетическая энергия остаётся ограниченной.

Поиск с участием людей. Над задачей одновременно работали порядка 10 000 агентов на внутренней модели, которую OpenAI называет значительно сильнее GPT-6 Astra. Агенты запускали код и обменивались результатами внутри групп. Исследователи через Codex собирали полезные находки и добавляли их в следующие промпты.

На решение Навье — Стокса ушло 2,7 млн сообщений агентов и около 130 млрд выходных токенов. Решение группа получила 5 сентября, после чего команда перешла к формализации доказательства. Эти сроки и расход вычислений приводит [OpenAI в описании исследования](https://openai.com/index/navier-stokes-solution/).

Проверка у себя. Lean проверяет доказательство, записанное в виде формального кода. OpenAI выложила проект `openai/NavierStokesAndEuler`: после установки elan из корня проекта выполняются `lake exe cache get`, затем `lake build`. Проект использует Lean 4.34.0-rc2, Mathlib и Lake, как указано в [инструкции сборки](https://github.com/openai/NavierStokesAndEuler).

Для отдельной проверки через Comparator нужны `landrun`, `lean4export` и `nanoda_bin` в `PATH`. После `lake exe cache get` запускается `lake exe comparator ComparatorChallenges/NavierStokes.json`, согласно [инструкции проверки формализации](https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/README.md).

Обучение внутренней модели началось 28 августа и на момент объявления 8 сентября продолжалось.