OpenAI публикует доказательство гипотезы Навье — Стокса и заявляет, что не станет претендовать на Премию тысячелетия

Когда OpenAI объявила на пресс-конференции, что внутренняя модель справилась с одной из самых сложных нерешенных математических задач, мы писали, что никто не видел самого доказательства.

Теперь это уже не так, и опубликованные материалы сужают суть заявлений иначе, чем это было преподнесено в анонсе. OpenAI разместила подробное описание, PDF-документ и формализацию рассуждений в Lean с публичным репозиторием на GitHub.

Формализация — это самая важная часть, поскольку доказательство в системе Lean может быть проверено машиной любым желающим, что избавляет от необходимости верить компании на слово в вопросах математики. По заявлению OpenAI, на формализацию и проверку с помощью GPT-6 Astra ушло еще 17 часов.

Сам результат заключается в том, что первоначально гладкая жидкость в состоянии покоя может развить сингулярность за конечное время. В интерпретации OpenAI это «решает проблему тысячелетия Навье — Стокса путем установления утверждения „C“ (а также „D“) в официальной формулировке Премии тысячелетия».

И затем, два абзаца спустя:

«Мы не намерены претендовать на Премию тысячелетия за этот результат».

Это предложение выполняет гораздо больше работы, чем сам анонс. Компания, которая несомненно решила бы задачу с призом в 1 миллион долларов и 26 годами неудачных попыток со стороны научного сообщества, обязательно заявила бы на него права и сделала бы это с удовольствием.

Отказ от этого — самый ясный сигнал о том, как сама OpenAI оценивает убедительность своих претензий на фоне формальных критериев премии.

Ключевой момент заключается в силе внешнего воздействия. На жидкость в исследовании OpenAI «постоянно воздействовала гладкая сила» — от состояния покоя и до формирования сингулярности.

Компания сама проводит это различие, описывая параллельную работу Левента Алпёдже и Тристана Бакмастера над уравнениями Эйлера, и отмечает, что исследованный ими вариант «был версией без внешнего воздействия, когда никакие внешние силы не прикладываются».

Удовлетворяет ли появление особой точки под воздействием приложенной силы формулировке Математического института Клэя — это вопрос, на котором держится все остальное, и решать его математикам, а не авторам технологической колонки.

Масштаб предпринятой попытки заслуживает отдельного рассказа. Около 10 000 параллельных агентов работали над задачей в течение примерно 88 часов, с 1 по 5 сентября, обработав 2,7 миллиона сообщений и сгенерировав около 130 миллиардов выходных токенов.

В работе использовалась не GPT-6 Astra, вышедшая на прошлой неделе, а внутренняя система, которую OpenAI описывает как значительно более мощную. Сама Astra была задействована лишь для проверки ответа.

За этим методом скрывается более масштабный сдвиг. Доказательство было получено не за счет долгого рассуждения одной модели, а силами целого роя моделей, работавших параллельно в течение трех с половиной дней. Затраты на вычисления при этом, по прежним оценкам OpenAI, исчисляются миллионами долларов.

Это принципиально иной исследовательский инструмент по сравнению с тем, по которому отрасль до сих пор оценивала производительность систем. Это намекает на то, что рубеж исследований смещается от того, насколько умна отдельная модель, к тому, сколько вычислительных ресурсов вы можете позволить себе направить на решение одной задачи.

Это также означает, что результаты подобного рода смогут воспроизводить только те организации, которые способны тратить средства на аналогичном уровне, что является не самым комфортным свойством для математики.

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

Теперь на опубликованной странице оба исследователя упоминаются в связи с параллельной работой над задачей Эйлера с внешним воздействием, а им предлагается признать приоритет в совместном заявлении. Компания, которая считала обвинения беспочвенными, обычно не реагирует предложением о признании приоритета всего за несколько дней.

То, что поддается проверке, и то, что проверить нельзя, теперь четко разведено. Математическую часть может проверить любой, кто готов запустить доказательство в Lean. Соответствует ли результат критериям тысячелетия — вопрос к Институту Клэя и математическому сообществу.

Происхождение же самих идей — это единственный аспект, который не способна прояснить никакая формализация, поскольку происхождение — это утверждение о процессе обучения, который никто за пределами компании не может проверить.