ИИ 9 октября 2026, 15:06 МСК

В доказательстве OpenAI по уравнениям Навье — Стокса нашли расхождение с Lean-версией

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

Проверка заняла у команды около двух недель, при этом использовались подсказки ChatGPT. Расхождение найдено в лемме 8.6: в текстовом доказательстве значение должно быть меньше m + 4, а в Lean-варианте — меньше m + 5, что математически слабее. Учёные подчёркивают, что это не опровержение и не означает ошибочности решения.

Руководитель команды Андерс Хансен предполагает, что ИИ при формализации мог обойти фрагмент, который не компилировался, отклонившись от текста. Кевин Баззард из Имперского колледжа Лондона уверен, что задача решена верно, но меньше уверен в корректности самого текстового доказательства. По словам Хансена, такие работы должны читать люди, что ложится нагрузкой на математиков. OpenAI сообщила New Scientist, что знает о несоответствии и оно не делает недействительным ни одну из версий.

• Лемма 8.6: m + 4 в тексте и m + 5 в Lean
• Поиск расхождений занял около двух недель
• У OpenAI на решение ушло 88 часов