OpenAI заявила о решении проблемы существования и гладкости решений уравнений Навье — Стокса, сформулированной 200 лет назад. Это одна из семи задач тысячелетия Института Клэя с наградой в $1 млн. Вместо того чтобы полагаться исключительно на человеческую теоретическую мысль, компания преподнесла это достижение как важную веху в применении передовых моделей рассуждения (reasoning models) для фундаментальной науки. По словам исследователя OpenAI Себастьена Бубека, команда начала обучать специализированную математическую модель 28 августа, узнав об аналогичных успехах внутри конкурирующей лаборатории Anthropic.
Чтобы получить строгое доказательство, OpenAI развернула оркестрацию мультиагентной архитектуры: от 1 000 параллельных агентов, непрерывно работавших на протяжении 50 часов, до пикового роя в 10 000 агентов. Как признал глава исследовательского направления OpenAI Марк Чен, полный перебор пространства поиска обошелся в миллионы долларов вычислительных затрат. Итогом работы стало машинно-верифицированное доказательство, формализованное в интерактивной системе доказательства теорем Lean.
Битва за научный приоритет
Анонс вызвал мгновенную волну споров в научном сообществе по поводу академической этики и авторских прав. Математик из Нью-Йоркского университета Тристан Бакмастер заявил, что OpenAI пошла на форсированный вычислительный спринт только после того, как узнала о его совместной работе с исследователем Anthropic Левентом Альпёге. В понедельник Бакмастер и Альпёге опубликовали собственные материалы с ключевыми продвижениями по задаче Навье — Стокса, отметив, что их рабочий процесс опирался на Claude и Codex.
Бакмастер утверждает, что OpenAI пыталась договориться об условиях публикации и предлагала вариант, при котором он выпустил бы статью о решении проблемы внутренней моделью OpenAI, исключив Альпёге из списка соавторов. Бубек и CEO OpenAI Сэм Альтман публично опровергли любые попытки исключения соавторов, защищая собственный исследовательский пайплайн.
«И в воскресенье утром мы получили финальное решение, полностью формализованное в Lean».
Помимо корпоративного соперничества и борьбы за престиж, автоматизированные решения сложных дифференциальных уравнений с верификацией в Lean имеют прямую коммерческую ценность. Владение методами решения нелинейных дифференциальных уравнений в частных производных и гидродинамики напрямую трансформирует гидрогазодинамические расчеты (CFD), промышленную аэродинамику и высокоточное моделирование физических систем. По мере того как ведущие лаборатории превращают фундаментальную математику в капиталоемкую гонку вычислительных мощностей, грань между подлинным научным открытием и агрессивным корпоративным перехватом инициативы становится все тоньше.