Математики нашли расхождения между доказательством OpenAI и его версией на Lean

Исследователи обнаружили, что формализованная версия заявленного OpenAI решения задачи Навье — Стокса в нескольких местах не соответствует доказательству на естественном языке. Это не опровергает результат, но показывает, что успешная проверка Lean-кода сама по себе не подтверждает корректность текстовой статьи.

Математики Александр Бастунис, Фабиан Чирчелли и Андерс Хансен опубликовали препринт, в котором сравнили текст заявленного OpenAI доказательства возникновения сингулярности в уравнениях Навье — Стокса с его формализацией на Lean — системе компьютерной проверки математических доказательств.

Одно из расхождений относится к лемме 8.6. В статье приведена оценка, требующая производных до порядка m + 4, тогда как соответствующие утверждения в Lean требуют производных до порядка m + 5 и поэтому доказывают более слабый результат. Авторы также нашли различия в оценке потока давления из формулы 10.19: формальная версия использует другую границу и иной математический аргумент.

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