В пространстве математических прорывов OpenAI вновь возникла неоднозначность: команда сопоставила опубликованное доказательство по уравнениям Навье–Стокса с его Lean‑версйей и выявила расхождения в нескольких ключевых моментах. По сути, машинная формализация в коде сужает область выводов, чем текстовый вариант, но это не является опровержением и не означает, что задача не решена. Эти расхождения создают почву для сомнений в полной эквивалентности между формализацией и изложением на естественном языке.

Процесс выявления расхождений занял у команды около двух недель. При этом в работе использовались подсказки языковой модели ChatGPT, а ранее известно, что решение задачи потребовало 88 часов у OpenAI. Эти цифры подчеркивают различие между человеческим трудом над доказательством и автоматизированной формализацией, которая может допускать упрощения в деталях.

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

Руководитель исследовательской группы Андерс Хансен объяснил, что неправильный перевод мог произойти из стремления ИИ сделать компьютерный код полностью самосогласованным и ошибкоустойчивым. При автоматической формализации ИИ может искать обходные пути, если встречает часть доказательства, которая не компилируется, даже если это ведет к отклонению от читаемого на естественном языке текста.

Климат дискуссии дополняют слова Кевина Баззарда из Имперского колледжа Лондона: можно надёжно формализовать в Lean формулировку теоремы и проверить её компиляцию, но это не гарантирует, что текстовое доказательство в PDF точно передаёт логику. По его словам, Lean‑код может быть внутренне согласован, но не обязательно передаёт всю логику оригинального изложения.