Доказательство OpenAI по Навье-Стоксу построено не тем методом, что заявляла компания: разбор 166 страниц

OpenAI объявила доказательство 8 сентября 2026 года. Собрал его рой примерно из 10 000 копий внутренней математической модели компании: 88 часов счёта и 130 млрд токенов. В самом тексте компания прямо и не раз писала, что идёт по программе Диего Кордобы и Луиса Мартинес-Сороа.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Спор теперь не о том, посчитала ли машина, а о том, что именно она доказала и чем это подтверждено.

Галочка Lean не про исходный текст. Lean проверяет формальную запись доказательства, а не прозу, из которой её перевели. Статья arXiv:2610.08144 (Бастунис, Чирчелли, Хансен) от 6 октября показывает это на месте: формализованная версия не соответствует словесному доказательству блоуапа, то есть момента, когда решение уравнения за конечное время уходит в бесконечность.

Закрыт не тот вариант задачи. OpenAI закрыла варианты (C) и (D) формулировки Чарльза Фефермана 2000 года, где блоуап допускается при гладкой внешней силе. Луис Сильвестре из Чикагского университета говорит, что задача Клэя в этой постановке закрыта, а главная задача про уравнения Навье-Стокса осталась открытой. Институт Клэя платит за неё $1 млн.

Авторы исходной программы оценивают вариант с силой по-разному: Диего Кордоба считает его осмысленным, потому что все известные жидкости находятся под какой-то внешней силой, а Луис Мартинес-Сороа напоминает, что другие группы работали именно над сценарием без силы.

Тристан Бакмастер из NYU и Левент Альпёге выложили свои три результата за несколько часов до анонса OpenAI: пористая среда, Буссинеск и трёхмерный Эйлер с блоуапом при гладкой силе. Блоуап для Буссинеска и Эйлера они получили 15 августа 2026 года, а 22 августа проверили в Lean. Работали с Claude и Codex, причём первый машинный текст Бакмастер называет худшим, что он читал, а собственный разбор Эйлера зовёт нейрослопом.

Проверить можно руками. Репозиторий github.com/openai/math открыт под Apache-2.0: 719 манускриптов в 372 семействах результатов, формализация в Lean есть примерно у 42% главных результатов. README сам предупреждает, что у неформализованных результатов возможны проблемы (срез 6 октября 2026 года).

Камилло Де Леллис из Institute for Advanced Study разрешения спора не ждёт: по его словам, это уже не вопрос проверяемых математических фактов.