Исследователи обнаружили расхождения между доказательством уравнений Навье — Стокса, опубликованным OpenAI, и его алгоритмической версией на языке Lean. Машинный вариант содержит более слабые математические утверждения в ряде ключевых фрагментов.
Основное внимание математиков привлекло доказательство леммы 8.6. В текстовой версии значение должно быть меньше m + 4, тогда как в коде Lean указано m + 5. Это делает машинный вариант менее строгим, так как он допускает больше возможных решений.
Руководитель группы проверки Андерс Хансен сообщил, что на выявление несоответствий ушло около двух недель. По его словам, использование языковых моделей для создания доказательств требует от математиков значительных усилий по их ручной проверке.
Специалисты предполагают, что ИИ мог изменить логику доказательства в процессе формализации, чтобы обеспечить компиляцию кода. В OpenAI подтвердили наличие несоответствий, однако заявили, что это не означает недействительность представленных доказательств.
