9 сентября 2026 г.
OpenAI заявила о решении задачи Навье — Стокса: доказательство выложено в Lean
Компания опубликовала 166 страниц доказательства и формализацию, которую можно проверить кодом.
Около 10 000 ИИ-агентов работали над доказательством одновременно. По данным OpenAI от 8 сентября, успешная группа нашла решение за 88 часов.
OpenAI заявляет о доказательстве вариантов C и D одной из семи «задач тысячелетия». В этих вариантах первоначально неподвижная жидкость под действием гладкой внешней силы за конечное время развивает сингулярность: решение теряет гладкость, хотя энергия остаётся конечной.
От поиска к проверке. По данным компании, внутренняя модель нашла доказательство 5 сентября. Затем формализация и проверка в Lean с GPT-6 Astra заняли ещё 17 часов. Lean проверяет математические рассуждения по формальным правилам.
Исследователи использовали Codex для объединения полезных промежуточных результатов разных групп и включали их в следующие промпты. Агенты общались между собой и запускали код. На задачу пришлось 2,7 млн сообщений и около 130 млрд выходных токенов.
Проверка у себя. Формализации опубликованы в репозитории `openai/NavierStokesAndEuler`. Для сборки нужны elan, Lean 4.34.0-rc2, Mathlib и Lake. Из корня репозитория выполняются `lake exe cache get`, затем `lake build`.
Для независимой проверки через Comparator инструкция OpenAI требует добавить `landrun`, `lean4export` и `nanoda_bin` в PATH. После `lake exe cache get` запускается `lake exe comparator ComparatorChallenges/NavierStokes.json`.
По подсчёту Прии Раман из Stanford Tech Review от 8 сентября, репозиторий содержит 35 731 теорему и лемму без учёта зависимостей.
Внутренняя модель, которую OpenAI оценивает как значительно сильнее GPT-6 Astra, продолжала обучение на момент объявления 8 сентября.
Первоисточник
