OpenAI решила задачу Навье-Стокса с Lean 4 доказательством
OpenAI объявила о решении задачи тысячелетия Навье-Стокса — и одновременно опубликовала формальное доказательство на Lean 4, верифицированное машиной.
Главное
8 сентября 2026 года OpenAI объявила, что внутренняя система ИИ построила доказательство — подкреплённое формализацией в proof assistant (помощнике доказательств) Lean — того, что уравнения Навье-Стокса, описывающие движение жидкостей, могут развить сингулярность за конечное время. Компания заявила, что результат закрывает одну из задач тысячелетия Института Клэя. Но самое недооценённое в этом событии — не сам математический прорыв, а то, как он был оформлен.
Когда OpenAI опубликовала своё доказательство того, что решения уравнений Навье-Стокса могут «взрываться» за конечное время, компания одновременно выложила формальное доказательство на Lean 4. Именно этот факт остаётся практически незамеченным на фоне споров о приоритете и этике.
Что такое Lean 4 и почему это важно
Lean 4 — это одновременно язык программирования и proof assistant (ассистент доказательств), предназначенный для формальной верификации математических утверждений.
Lean 4 является одновременно языком программирования и ассистентом доказательств, созданным для формальной верификации. Каждая теорема или программа, написанная на Lean 4, должна пройти строгую проверку типов доверенным ядром системы, давая бинарный вердикт: утверждение либо верно, либо нет. Такая проверка «всё или ничего» не оставляет места для неоднозначности.
Иными словами, Lean 4 предоставляет среду, где корректность математически гарантирована, а не просто предполагается.
До самого последнего времени генерация верифицируемых машиной формальных доказательств была мучительно трудоёмкой задачей. Теперь ИИ меняет это уравнение.
Как проходил процесс
Система OpenAI создала аналитическое доказательство и его формализацию на Lean, подтверждающие, что изначально гладкая жидкость в состоянии покоя способна развить сингулярность за конечное время.
Агенты пришли к решению задачи Навье-Стокса 5 сентября 2026 года, примерно через 88 часов после запуска первых агентов; формализация и верификация на Lean заняли дополнительно 17 часов — их выполнила модель GPT-6 Astra.
По описанию OpenAI, над задачей Навье-Стокса работало порядка 10 000 одновременных агентов с использованием внутренней модели, более мощной, чем GPT-6 Astra.
graph TD
A["1 сентября: старт агентов"] --> B["~50 ч: решение уравнений Эйлера (Euler)"]
B --> C["5 сентября: доказательство Навье-Стокса\n(88 часов)"]
C --> D["GPT-6 Astra: формализация на Lean 4\n(+17 часов)"]
D --> E["8 сентября: публикация\nдоказательства + Lean-кода"]
style E fill:#22c55e,color:#fff
Суммарно по всем задачам агенты отправили 4,9 миллиона сообщений и использовали около 300 миллиардов выходных токенов; на Навье-Стокс пришлось 2,7 миллиона сообщений и примерно 130 миллиардов токенов.
Что лежит в открытом доступе
Репозиторий содержит формализации на Lean 4 результатов, представленных в работах «Finite time blowup for Navier–Stokes» и «Finite time blowup for the Euler equation» за авторством OpenAI.
OpenAI опубликовала 166-страничную статью о Навье-Стокс вместе с открытыми файлами Lean-доказательств.
-- Пример структуры Lean 4 формализации
theorem navier_stokes_blowup
(viscosity : ℝ) (hv : 0 < viscosity) :
∃ (initial_data forcing : SmoothData),
¬ GlobalSmoothSolution initial_data forcing := by
-- машинно-верифицированное доказательство
sorry
| Что опубликовано | Формат | Доступность |
|---|---|---|
| Аналитическое доказательство | PDF, 166 страниц | Открытый |
| Lean 4 формализация | Репозиторий GitHub | Открытый |
| Описание агентного процесса | Блог OpenAI | Открытый |
| Внутренняя модель (умнее GPT-6 Astra) | — | Закрытый |
Параллельная история: спор о приоритете
В тени прорыва разгорелся крупный этический конфликт.
Математик Тристан Бакмастер из Нью-Йоркского университета и Левент Альпёге, исследователь из компании Anthropic — конкурента OpenAI, — достигли значительного прогресса в решении задачи за последний месяц, используя AI-инструменты от OpenAI и Anthropic.
Бакмастер и Альпёге смогли верифицировать корректность своего доказательства с помощью языка программирования Lean, однако текстовое объяснение, сгенерированное языковыми моделями, было едва читаемым.
Прежде чем они успели опубликовать свои находки, OpenAI предприняла собственные масштабные усилия — вложив миллионы долларов вычислительных ресурсов в задачу. OpenAI утверждает, что намеренно не использовала последние работы Бакмастера и Альпёге, однако Бакмастер выпустил публичные заявления, ставящие под сомнение эту позицию.
Почему Lean 4 — это тихая революция
Аспект работы OpenAI, о котором почти никто не говорит: компания опубликовала формальное доказательство на Lean 4 одновременно с обычным, читаемым людьми доказательством. Немало других математических гипотез было недавно закрыто с помощью ИИ, и они также сопровождались формальными доказательствами — в частности, на Lean 4.
Если каждый математический результат, полученный с помощью ИИ, будет сопровождаться машинно-верифицированным доказательством, стандарты надёжности в математике изменятся навсегда.
Исследования демонстрируют, что сочетание больших языковых моделей с ассистентом формальных доказательств, таким как Lean 4, способно существенно расширить возможности ИИ в математическом рассуждении.
Сочетание единого языка, глубокой математической библиотеки и программного инструментария сделало Lean 4 фокусной точкой современных AI-методов доказательства.
Итог
История с Навье-Стокс имеет два уровня. Первый — громкий: ИИ-агенты за 88 часов решили задачу, над которой математики бились 90 лет. Второй — тихий, но потенциально более важный: OpenAI одновременно опубликовала как описание доказательства, так и его формализацию на Lean. Это делает результат верифицируемым не людьми-рецензентами, а математически строгой машиной. Если тенденция закрепится, будущее фундаментальной математики будет писаться совместно — людьми, ИИ и proof assistant’ами.