OpenAI заявила о решении задачи тысячелетия: доказательство выложено в Lean

Уравнения Навье — Стокса описывают движение жидкости и газа. OpenAI заявляет, что построила течение, в котором скорость становится неограниченной за конечное время, хотя энергия остаётся ограниченной, а внешняя сила меняется плавно. Компания относит результат к вариантам C и D задачи тысячелетия. [Описание результата OpenAI](https://openai.com/index/navier-stokes-solution/).

Ранее математик Нью-Йоркского университета Тристан Бакмастер и сотрудник Anthropic Левент Альпьоге получили результаты для родственных уравнений с помощью Claude и Codex, прежде всего GPT-5.6 Sol. По словам Бакмастера, результаты для уравнений Буссинеска и Эйлера были готовы 15 августа, а проверка в Lean завершилась 22 августа. Исходную идею он приписывает математикам Диего Кордобе и Луису Мартинесу-Сороа. [Заявление Бакмастера от 8 сентября](https://mastodon.social/@tristanbuckmaster/117233413705701198).

OpenAI датирует начало своего эксперимента 1 сентября, после слухов о решении задач тысячелетия. Компания использовала внутреннюю модель, которую называет значительно сильнее GPT-6 Astra, а через Codex объединяла промежуточные результаты групп агентов. На задачу ушло 130 млрд выходных токенов. [Хронология и расход вычислений OpenAI](https://openai.com/index/navier-stokes-solution/).

Спор об авторстве. Бакмастер утверждает, что сотрудник OpenAI Себастьен Бубек дважды предлагал исключить Альпьоге из авторов совместной статьи из-за его работы в Anthropic. Бакмастер также сообщил о загрузке черновиков в Codex, прямо уточнив, что не знает, использовала ли компания эти материалы. [Позиция Бакмастера](https://mastodon.social/@tristanbuckmaster/117233413705701198).

OpenAI отрицает доступ сотрудников и агентов к неопубликованной работе математиков и использование конкретных пользовательских данных для решения задачи. При этом компания допускает, что обезличенные данные использования её продуктов могли помочь улучшить модели. [Ответ OpenAI](https://openai.com/index/navier-stokes-solution/).

Проверка на компьютере. OpenAI опубликовала доказательства в NavierStokesAndEuler в формате Lean, системы машинной проверки математических рассуждений. Для сборки нужны elan и указанная в проекте версия Lean 4.34.0-rc2. Из корня репозитория выполняются команды `lake exe cache get`, затем `lake build`. [Репозиторий и инструкция сборки](https://github.com/openai/NavierStokesAndEuler/blob/main/README.md).

Для отдельной проверки формализации авторы также опубликовали [инструкцию запуска Comparator](https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/README.md).