OpenAI 8 сентября опубликовала математическую работу на 165 страницах и её формализацию в Lean — системе для машинной проверки доказательств. По заявлению компании, её внутренняя ИИ-система получила решение проблемы существования и гладкости уравнений Навье—Стокса, одной из задач тысячелетия. Сообщение OpenAI.

Уравнения Навье—Стокса описывают движение вязкой жидкости. Вязкость сглаживает различия в скорости между соседними участками потока. Фундаментальный вопрос — гарантирует ли это сохранение гладкого течения на любое время вперёд. Именно учёт вязкости отличает новую работу от результата Бакмастера и Алпёге по уравнениям Эйлера, о котором мы писали ранее.

В опубликованной работе построен сценарий, в котором жидкость сначала покоится, а затем под действием гладкой внешней силы образует вихрь. Область интенсивного движения сжимается, и за конечное время скорость в ней становится неограниченной, хотя суммарная кинетическая энергия остаётся ограниченной. Такой пример предложен для любой положительной вязкости. Гладкая внешняя сила прямо допускается вариантами C и D официальной задачи Clay, на решение которых претендует работа. Препринт, формулировка Clay.

По отчёту OpenAI, результат получила группа примерно из 10 тысяч одновременно работающих ИИ-агентов на основе внутренней модели. Исследователи направляли поиск и объединяли промежуточные находки разных групп. На получение доказательства ушло около 88 часов после запуска первых агентов, ещё 17 часов — на формализацию и проверку в Lean. Отчёт компании.

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

Иллюстрация: схема развития вихря из работы OpenAI (рисунок 1).