Статья на arXiv: Lean-версия доказательства OpenAI по Навье, Стоксу не совпадает с оригиналом
На arXiv (раздел математики, анализ уравнений в частных производных) 6 октября 2026 года появился препринт «Navier-Stokes lost in translation» («Навье, Стокс, потерянный в переводе»). Его тема: автоформализация, то есть перевод математического текста с естественного языка на формальный язык вроде Lean, всё чаще используют, чтобы проверять математические тексты, в том числе написанные ИИ. Среди примеров в аннотации, объявленное OpenAI доказательство blow-up решений уравнений Навье, Стокса.
Схема такая: ИИ-система переводит текст с естественного языка на Lean, после чего записанное на формальном языке рассуждение можно легко проверить автоматически. Цель статьи, по словам авторов, показать, почему такой процесс может не давать никакой уверенности в исходном рассуждении на естественном языке: перевести семантически верно, то есть сохранив смысл, трудно.
Теоретический довод авторов: задача разрешения неоднозначностей в математическом тексте на естественном языке, необходимая для семантически верного перевода, находится сколь угодно высоко в иерархии Solvability Complexity Index (SCI, индекс сложности разрешимости) и арифметической иерархии; авторы пишут, что SCI для неё равен бесконечности. Для сравнения, у проблемы остановки (Halting problem) SCI равен 1. Отсюда авторы делают неформальный вывод: обеспечить семантически верную ИИ-автоформализацию сложнее, чем решить любую вычислимую задачу, включая проблему остановки. Это сформулировано как неформальное пояснение, а не как строгая теорема.
На практике авторы приводят несколько примеров ошибочных ИИ-переводов утверждений и доказательств с естественного языка на Lean. В результате получаются несоответствия между доказательствами на естественном языке и их «проверками» на Lean. В число примеров входит объявленное OpenAI доказательство для уравнений Навье, Стокса: авторы показывают, что формализованное на Lean доказательство не соответствует доказательству blow-up решений этих уравнений на естественном языке.
Важная оговорка: в аннотации не сказано, верно или неверно само исходное доказательство на естественном языке. Говорится лишь, что его Lean-версия ему не соответствует, а проверка «может» не давать уверенности, но не «никогда» её не даёт.
Ключевые факты
- Препринт на arXiv от 6 октября 2026 года (math.AP) утверждает, что автоформализация на Lean может не давать уверенности в исходном доказательстве на естественном языке.
- Главный пример, объявленное OpenAI доказательство blow-up решений уравнений Навье, Стокса: по словам авторов, его Lean-версия не соответствует доказательству на естественном языке.
- Теоретический довод: задача разрешения неоднозначностей в математическом тексте имеет SCI, равный бесконечности, тогда как у проблемы остановки SCI равен 1.
- Неформальный вывод авторов: семантически верная ИИ-автоформализация сложнее любой вычислимой задачи, включая проблему остановки.
- Помимо примера с OpenAI, в статье есть ещё несколько случаев ошибочных ИИ-переводов утверждений и доказательств на Lean.
Почему это важно
Формальная проверка на Lean считается надёжным способом убедиться в математическом результате, и её всё чаще применяют к текстам, написанным ИИ. Авторы статьи указывают на слабое место: проверяется не исходное рассуждение, а его перевод, выполненный ИИ. Если перевод неточен, успешная машинная проверка говорит о формализованной версии, а не об оригинале. Особенно заметно это на примере громко анонсированного доказательства OpenAI по уравнениям Навье, Стокса.
Кому это важно
Математикам, которые читают и проверяют ИИ-доказательства; разработчикам систем автоформализации и ИИ-помощников для доказательств на Lean; редакторам и журналистам, которые освещают заявления вроде «ИИ доказал…» и опираются на «зелёную галочку» формальной проверки; всем, кто следит за заявлениями OpenAI о научных результатах.
Как это применить
Практический вывод из аннотации: не считать успешную проверку на Lean автоматическим подтверждением доказательства на естественном языке. Нужно отдельно убедиться, что формальные утверждения действительно выражают то, что утверждается в исходном тексте. Как именно это делать, в аннотации не расписано, подробности есть в полном тексте статьи (PDF/HTML на arXiv).
Можно ли доверять
Это препринт: на arXiv он размещён 6 октября 2026 года и, судя по имеющемуся тексту, не рецензирован. Мы пересказываем только аннотацию. В ней не перечислены авторы (в истории подачи указан лишь отправивший версию v1, Alexander Bastounis), не названы использованные ИИ-система и версия Lean, не уточнено число примеров, кроме слова «несколько». Не сказано, когда OpenAI объявила своё доказательство и ответила ли компания на критику. Утверждение о том, что семантически верная автоформализация «сложнее проблемы остановки», авторы называют неформальным.
Риски и подводные камни
Статья не говорит, что исходное доказательство OpenAI неверно: утверждается лишь, что его Lean-версия ему не соответствует. Не стоит читать это как опровержение результата. Формулировка о «сложности выше проблемы остановки» неформальная, её не следует воспринимать как строгую теорему. Кроме того, авторы пишут, что проверка «может» не давать уверенности, а не что она не даёт её никогда. Оценить аргументацию целиком можно только по полному тексту.
«Мы показываем, что формализованное доказательство на Lean не соответствует доказательству на естественном языке для blow-up решений уравнений Навье, Стокса.»
— Из аннотации статьи «Navier-Stokes lost in translation», arXiv