Доказательство ИИ можно проверить кодом: OpenAI опубликовала решение задачи Навье–Стокса

Поиск и проверка. Решение получила внутренняя модель, которую OpenAI называет значительно сильнее GPT-6 Astra. Затем GPT-6 Astra помогла формализовать и проверить доказательство в Lean, что заняло ещё 17 часов. В Lean математические рассуждения записывают так, чтобы компьютер мог проверить каждый шаг.

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

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

На задачу Навье–Стокса агенты потратили около 130 млрд выходных токенов и отправили 2,7 млн сообщений. Вся исследовательская работа по нескольким задачам потребовала около 300 млрд токенов и 4,9 млн сообщений.

Проверка у себя. Формализация доступна в репозитории OpenAI `openai/NavierStokesAndEuler` на GitHub. Для сборки нужны elan и Lean 4.34.0-rc2 с зависимостями проекта. Из корня репозитория выполняются команды:

```sh lake exe cache get lake build ```

Для отдельной проверки через Comparator инструкция требует добавить в PATH инструменты `landrun`, `lean4export` и `nanoda_bin`. После загрузки кеша команда запуска выглядит так:

```sh lake exe comparator ComparatorChallenges/NavierStokes.json ```

В PDF физическое описание начинается на странице 3, схема доказательства на странице 6. Для связанной задачи Euler с внешней силой OpenAI признала приоритет Левента Альпёге из Anthropic и Тристана Бакмастера из NYU. Собственный результат компании для Euler относится к случаю без внешней силы.

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