OpenAI представила предполагаемое решение задачи Навье—Стокса — одной из семи «задач тысячелетия». В компании утверждают, что внутренний ИИ построил доказательство и записал его в системе проверки Lean.
Уравнения Навье—Стокса описывают движение жидкостей и газов. Они используются в проектировании самолетов, прогнозировании погоды и анализе кровотока. Нерешенный вопрос состоит в том, всегда ли изначально гладкое течение остается таким или в нем за конечное время может возникнуть сингулярность — точка, где скорость становится неограниченной.
Система OpenAI предложила контрпример. В нем жидкость сначала покоится, но под действием гладкой внешней силы образует закручивающийся внутрь вихрь. Его центральная область сужается и ускоряется, пока скорость не становится неограниченной. Энергия при этом остается конечной.
Компания сообщила, что ИИ-агенты перебирали подходы ко всем задачам тысячелетия. Работа над результатом по Навье—Стоксу заняла около 88 часов, еще 17 часов потребовались на формализацию и проверку в Lean. Система сгенерировала около 130 млрд выходных токенов в 2,7 млн сообщений.
Но проверка кода не закрыла научный спор. Александр Бастунис, Фабиан Чирчелли и Андерс Хансен, исследователи математических доказательств, указали на расхождения между обычным текстом работы и формулировками в Lean. Среди претензий — разные требования к производным и несоответствие в оценке потока давления.
Lean подтверждает только то утверждение, которое в него точно записали. Если формальная версия отличается от исходного доказательства, успешно проверенный файл не доказывает корректность всей статьи.
OpenAI сама не претендует на премию Института Клэя. Сейчас подтвержден лишь факт публикации предполагаемого решения. Статуса признанной теоремы у него нет.
