Код для компьютерной проверки доказательства OpenAI о Навье — Стоксе расходится со статьёй

Код в Lean¹, которым OpenAI подкрепила своё доказательство для уравнений Навье — Стокса², местами доказывает не то, что написано в статье. Это показали в препринте трое математиков, среди них профессор Кембриджа Андерс Хансен.

Почему это важно: перевод в Lean всё чаще считают надёжной проверкой доказательств, которые пишет ИИ. Авторы показывают, что принятый Lean код подтверждает итоговую теорему, но не рассуждения, которые читают математики.

Предыстория: 8 сентября OpenAI объявила, что её внутренняя модель доказала: решения уравнений Навье — Стокса с внешней силой могут за конечное время разрушиться — скорость жидкости становится бесконечной. Над доказательством 88 часов работали 10 000 ИИ-агентов, а GPT-6 Astra за 17 часов перевела его в Lean.

Повод: авторы вручную сверили статью OpenAI с кодом из репозитория компании и описали два расхождения:

• В лемме 8.6 статье хватает четырёх дополнительных производных функции, а код в Lean требует пять, то есть ставит более строгое условие и доказывает более слабое утверждение. Пять производных вместо четырёх код требует и в других своих местах.
• Одну из оценок, нужных для доказательства единственности решения, код получает другим путём, и в эту оценку входит величина, которой в статье нет, поэтому версии статьи и кода трудно сравнить.

Других расхождений два разобранных примера не исключают: ручная сверка идёт медленно, пишут авторы.

Детали: успехом при переводе считается код, который Lean принял. Совпадает ли он с текстом, проверка не смотрит. В примере авторов чат-бот получил доказательство неравенства для многочлена третьей степени с неверными кратностями корней и вернул правильный код в Lean: сам нашёл верные кратности, а доказательство в тексте так и осталось ошибочным.

Общая картина: авторы доказывают, что в общем случае ни один алгоритм не может перевести математический текст в Lean без потери смысла: эта задача сложнее проблемы остановки³. Пример — число из учебника, заданное как наименьшее n, при котором некое уравнение не имеет решений в натуральных числах. Если такого n нет, стандартная функция Lean молча подставит ноль, и простое алгебраическое равенство с этим числом пройдёт проверку, хотя самого числа нет.

Но: что статья OpenAI неверна, авторы не утверждают. «Мы не делаем заявлений о правильности доказательства OpenAI, написанного обычным языком, — только об ошибках перевода в Lean», — пишут они. По их мнению, такие доказательства нужно рецензировать так же, как любые другие.

Что говорят: на Hacker News⁴ значение находки оспаривают. «Скорее всего, промежуточные утверждения не совпадают, но итоговый результат всё равно верен», — считает один из пользователей. «У OpenAI есть доказательство формулировки в Lean. Больше им ничего не нужно», — пишет другой.

Так уже было: весной 2026 года Meta* заявила, что перевела в Lean 26 учебников математики — около 500 000 строк кода. Участники сообщества Lean быстро нашли грубые ошибки: «На деле точно формализовано 0% утверждений», — написал об одном из учебников Джек Маккарти. Ловить такие ошибки будет всё труднее, предупреждают авторы: формализация Великой теоремы Ферма у Anthropic заняла 13 млн строк кода Lean.

Что дальше: авторы ждут похожих расхождений во втором доказательстве OpenAI — о разрушении решений уравнений Эйлера — и называют их вероятность «очень высокой». Как строить автоформализаторы, которые сохраняют смысл текста, они обещают показать в следующих статьях.