Навье—Стокс: доказательство потерялось при переводе в код?

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

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

⚠️ Авторы новой работы обнаружили расхождения между текстом и Lean-кодом. В одном из примеров текстовое доказательство требует оценку с m + 4 дополнительными производными, тогда как в формализации доказывается вариант с m + 5. Это не косметическая разница: формально проверенный код и опубликованное математическое рассуждение оказываются не одним и тем же объектом.

Значит ли это, что доказательство OpenAI неверно? Нет — авторы статьи этого не утверждают. Их тезис в том, Lean-код может корректно компилироваться и доказывать некоторое формальное утверждение, но из этого не следует, что он корректно перевёл человеческий текст и подтвердил именно заявленный результат.

→ Здесь есть четыре разных слоя: исходная задача; текстовое доказательство; формальное утверждение; код, который фактически проверил Lean. Между ними нужно доказать соответствие — и этот шаг нельзя автоматически получить из того, что программа не выдала ошибку.

Это ровно то различие, о котором мы писали раньше: формальная верификация чрезвычайно сильна, но не является магической печатью «истинно». Она проверяет формализованный объект. Кто-то — пока человек, а в будущем, возможно, более надёжная система агентов — должен ещё проверить, что этот объект действительно выражает нужную теорему и нужный аргумент.

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

Это не отменяет ценности формализации. Напротив: такой сбой стал виден именно потому, что и текст, и код оказались доступны для разбора. Но он показывает, что в новой математической инфраструктуре нужно проверять не только доказательства, а переводы между всеми языками, на которых существует знание.