OpenAI представила 166-страничное доказательство для одного из вариантов задачи о трёхмерных уравнениях Навье — Стокса, относящейся к проблемам тысячелетия. Компания заявила, что её внутренняя система построила пример, где гладкая жидкость под действием гладкой внешней силы за конечное время достигает бесконечной скорости при конечной энергии. Значение истории не сводится к скорости работы агентов: опубликованный материал пока не означает окончательного решения задачи тысячелетия, а проверка выявила границу между текстовым рассуждением и тем, что формально подтверждено в Lean.

Согласно описанию опубликованного доказательства, OpenAI заявляла доказательство вариантов C и D в формулировке задачи. Это существенно уже привычного тезиса о том, что вопрос о гладкости решений Навье — Стокса полностью закрыт. В найденном сценарии речь идёт не о произвольном течении, а о специально сконструированном примере с гладкой внешней силой. Именно условия задачи и допустимость такого примера определяют, соответствует ли результат критериям Института математики Клэя.

Как был получен результат.

По данным OpenAI, на поиск работала система примерно из 10 тысяч параллельных агентов. На построение примера ушло 88 часов, затем ещё 17 часов заняла формализация в Lean. Как пишет Science Mail, в процессе агенты обменялись 2,7 миллиона сообщений и сгенерировали около 130 миллиардов выходных токенов непосредственно по задаче Навье — Стокса. Это не один запрос к языковой модели, а распределённый поиск, где множество агентов развивают, отбрасывают и сопоставляют разные линии аргументации.

Перед этим система работала с родственными уравнениями Эйлера, где не учитывается вязкость. По данным разбора DataCamp, этот этап дал агентам промежуточный механизм, после чего вычислительные ресурсы перевели на Навье — Стокса. Такой порядок показывает возможную практическую схему применения LLM в фундаментальной математике: не мгновенная генерация готовой теоремы, а серия связанных поисков, где результат в более простой модели становится опорой для следующей задачи.

Почему Lean не снял все вопросы.

Формальная проверка важна, но она подтверждает конкретный набор утверждений, записанный в коде, а не автоматически весь естественно-языковой текст статьи. Группа Александра Бастуниса, Фабиана Чирчелли и Андерса Хансена сопоставила текст OpenAI с Lean-версией. Как следует из публикации о сравнении двух версий, в одном фрагменте статья обещает оценку с четырьмя дополнительными производными, тогда как формальная конструкция требует пяти. В другом месте расходятся условия и структура оценки.

Авторы анализа не объявляли словесное доказательство неверным. Их вывод уже: Lean-код сам по себе не служит подтверждением каждого написанного в статье предложения. Для разработчиков формальных методов это знакомое различие между доказательством в публикации, его формализацией и утверждением, которое в итоге проверяет система. Для исследовательских AI-команд оно означает, что открытого репозитория с кодом недостаточно без трассировки: какой именно фрагмент статьи соответствует каждой лемме и где менялись допущения.

Спор о приоритете и данных.

Анонс OpenAI совпал с конфликтом вокруг работ Тристана Бакмастера из Нью-Йоркского университета и Левента Альпеге из Anthropic. Они разрабатывали близкий подход и утверждали, что компания узнала о нём до собственного объявления. В изложении позиции Бакмастера говорится, что его ранний вариант, полученный с помощью LLM, требовал последующей проверки в Lean, а публикацию ускорили слухи о предстоящем результате OpenAI. Компания, по сообщениям источников, отвергала доступ к неопубликованным материалам математиков.

Из доступного сравнения следует, что маршруты доказательств не совпадают буквально: эксперты, изучавшие текст OpenAI около месяца, не нашли простого воспроизведения пути Бакмастера и Альпеге. Однако отсутствие буквального совпадения не закрывает вопрос об условиях научного приоритета, использовании взаимодействий с продуктами и коммуникации между компаниями и авторами. Обзор конфликта также указывает, что независимая проверка самого результата ещё продолжается.

Что это меняет для рынка AI.

История показывает сдвиг от демонстраций решения олимпиадных задач к дорогостоящим исследовательским конвейерам: тысячи агентов, специализированные инструменты, программные проверки и экспертный разбор. При этом вычислительный масштаб не заменяет научную экспертизу. Сообщения о стоимости эксперимента, приведённые в оценке DataCamp, относятся к серии запусков и не делают математический вывод более или менее верным.

Практический вывод для команд, внедряющих LLM в R&D, состоит в разделении трёх результатов: найденной гипотезы, человечески читаемого доказательства и формально проверенного утверждения. Они могут появляться в разное время и иметь разный объём. Для OpenAI эта работа стала демонстрацией агентного поиска и формализации; для математического сообщества — материалом для независимой проверки. До её завершения корректно говорить о заявленном доказательстве специального сценария, а не о бесспорно решённой проблеме тысячелетия.