Навье–Стокс и доказательство на Lean: вынужденные особенности и непрозрачность лаборатории

8 сентября 2026 года OpenAI заявила, что её внутренняя модель, никогда не выпускавшаяся публично, получила доказательство взрыва за конечное время для трёхмерных несжимаемых уравнений Навье–Стокса. Компания опубликовала теоретический документ и открытый репозиторий NavierStokesAndEuler, содержащий формализацию на языке Lean 4 теорем о гладких начальных данных под действием внешнего вынуждающего члена. По изложению самой лаборатории, результат покрывает утверждения о потере регулярности из формулировки, составленной математиком Чарльзом Фефферманом для Институт Клэя, но не затрагивает случай без внешней силы, который научное сообщество считает более трудным вариантом задачи. Автор официальной формулировки назвал решение волнующим, упомянув вклад Кордобы и Мартинеса-Сороа, тогда как компания с самого начала пояснила, что не намерена претендовать на приз в миллион долларов.

Эта история сплетает автоматизацию математики со сроками академических институтов. Институт Клэя по-прежнему числит Навье–Стокса среди нерешённых задач: регламент требует публикации в квалифицированном издании, выдержки не менее двух лет с момента публикации и общего признания математическим сообществом, а по существу институт до сих пор не высказался. Его президент Мартин Бридсон напомнил, что оценка намеренно идёт неспешно, чтобы обеспечить абсолютную строгость. Картину усложняет спор о приоритете с параллельной работой, о которой рассказал математик Теренс Тао и которую сами авторы описывают как в значительной мере выполненную с помощью искусственного интеллекта. Математик из Нью-Йоркского университета оспорил изложение контактов, данное лабораторией, предположив, что к результату могли причаститься закрытые сессии проприетарного инструмента; компания отрицает, что видела неопубликованную работу напрямую, но признаёт, что не может исключить влияние обезличенных данных использования на обучение собственных моделей.

В репозитории указаны инструкции, позволяющие перепроверить доказательство машиной, однако ни одна независимая проверка до сих пор не завершена; помимо этой проверки, проприетарный характер использованной инфраструктуры делает невозможной любую независимую верификацию затрат и выставляемых напоказ показателей эффективности. Заявленные вычисления — около десяти тысяч одновременно работающих агентов с 1 по 5 сентября, 88 часов до получения доказательства и ещё 17 на формализацию и проверку в Lean — остаются корпоративными утверждениями, которые извне никто не может воспроизвести. Без доступа к обучающему коду или к весам системы научное сообщество способно подтвердить лишь формальные шаги, выложенные в репозитории; реальные условия воспроизводимости эксперимента остаются в тени.

Формальная математика обрела грозного союзника в автоматической проверке логических переходов, но гонка за научное первенство на закрытых моделях обнажает свои структурные пределы. Проверить теорему — теперь задача, которую выполняет машина; установить прозрачность цепочки, породившей её, по-прежнему требует вполне человеческой строгости.

— Olya