Компания OpenAI сообщила о значимом достижении в области автоматизированных математических доказательств: передовая внутренняя языковая модель и сеть ИИ-агентов подготовили проект решения проблемы существования и гладкости решений уравнений Навье — Стокса. Данная математическая задача входит в официальный список семи задач тысячелетия, за доказательство каждой из которых Математический институт Клэя в 2000 году назначил премию в один миллион долларов.
Согласно опубликованным данным, исследовательский процесс задействовал масштабные вычислительные ресурсы. Запуск специализированных агентов стартовал 1 сентября 2026 года после поступления слухов о возможных прорывах в этой сфере. Система достигла результата за 88 часов, после чего потребовалось еще 17 часов на формализацию и проверку доказательства в ассистенте доказательств Lean с помощью модели GPT-6 Astra. По оценкам экспертов, масштабы генерации беспрецедентны: в процессе решения агенты отправили около 2,7 миллиона сообщений и израсходовали примерно 130 миллиардов выходных токенов.
Хотя технические параметры закрытой внутренней модели не раскрываются полностью, расчеты на основе публичных тарифов аналогичных frontier-моделей показывают, что подобный объем генерации требует колоссальных затрат. Представители компании уже заявили, что в случае официального признания доказательства они не будут претендовать на денежный приз Клэя, однако само событие мгновенно привлекло внимание академического сообщества и спровоцировало жесткие дискуссии о конфиденциальности научных разработок.
Споры о приоритете и методах работы исследователей
Публикация OpenAI совпала по времени с резкими обвинениями со стороны Тристана Бакмастера, профессора математики Нью-Йоркского университета, который в течение почти года работал над родственными задачами в сотрудничестве с Левентом Алпёге, математиком из компании Anthropic. По словам Бакмастера, их исследовательская группа на протяжении месяцев активно использовала для обсуждений и черновиков коммерческие инструменты, включая Claude и Codex, а также модель GPT-5.6 Sol.
Когда математическое сообщество заполнили слухи о готовящихся результатах, авторы связались с лабораторией и выяснили, что параллельная команда OpenAI вела аналогичные изыскания. Вопросы вызвали сроки запуска агентов OpenAI, которые приступили к активной фазе работы лишь после того, как в прессу или в поле слухов попали сведения о деятельности группы Бакмастера и Алпёге.
В ответ на запросы руководство OpenAI подчеркнуло, что исследователи и агенты компании не имели прямого доступа к закрытым сессиям пользователей. Тем не менее, официальная позиция лаборатории допускает, что обезличенные данные, поступающие от пользователей продуктов компании, теоретически могли косвенно способствовать улучшению общих характеристик моделей. Представители лаборатории также указали на содержательные отличия в полученных математических выкладках, отметив, что их доказательство строится иначе и охгрывает другие частные случаи в задачах Эйлера.
Риски для открытой науки и экосистемы исследователей
Ситуация вокруг решения Навье — Стокса ярко продемонстрировала фундаментальный сдвиг в правилах игры для академического мира. Известный математик Теренс Тао публично отметил, что распространение слухов о перспективных направлениях работы теперь способно мгновенно спровоцировать массивную автоматизированную атакуfrontier-моделей на ту же проблему.
Подобная динамика создает серьезные стимулы для ученых полностью отказаться от традиций открытой науки. Когда предварительный обмен идеями или случайная утечка информации могут привести к тому, что технологический гигант задействует кластер из тысяч ИИ-агентов и опередит авторов на финишной прямой, исследователи неизбежно перейдут к режиму строгой изоляции. В компьютерной безопасности аналогичный тренд уже привел к тому, что слух об уязвимости заставляет защитников и атакующих в спешке искать эксплойты с помощью автономных агентов. Теперь аналогичная угроза нависла над фундаментальной математикой.
Проверка доказательства и статус формализации в Lean
Важной особенностью проекта OpenAI стала опора на автоматизированную верификацию. Создание корректного аналитического текста в сотни страниц не гарантирует отсутствие скрытых логических ошибок, поэтому команда использовала среду Lean для машинной проверки каждого шага.
Тем не менее, экспертное сообщество напоминает о разнице между механически верифицированным машинным кодом и принятием решения математическим институтом. Формальное доказательство в Lean проверяет соответствие кода заданным правилам синтаксиса и логики, но не заменяет глубокую научную экспертизу со стороны независимых математиков. Признание решения задачи Навье — Стокса требует многомесячного или даже многолетнего изучения специалистами по дифференциальным уравнениям в частных производных.
Практические выводы для разработчиков и исследователей
Событие задает новую реальность для всех, кто использует языковые модели для работы над конфиденциальными проектами, интеллектуальной собственностью и нераскрытыми алгоритмами:
Управление рисками утечки контекста. Если исследователи обсуждают прорывные идеи внутри платформ общего назначения, существует теоретический и практический риск того, что накопленный датасет взаимодействий повлияет на будущие итерации базовых моделей компании-разработчика.
2. Необходимость локальных и защищенных контуров. Проекты, находящиеся на стадии патентования или глубокой научной разработки, требуют использования полностью изолированных локальных моделей или жестких корпоративных контрактов с гарантированным исключением пользовательских логов из процессов обучения.
3. Ускорение горизонта планирования. Наличие агентов, способных тратить миллиарды токенов на узкоспециализированный поиск доказательств, означает, что любое открытое обсуждение сложной задачи должно завершаться быстрой публикацией препринта, иначе автоматизированные системы конкурентов могут закрыть проблему быстрее людей.