Задачу тысячелетия Navier–Stokes закрыла модель OpenAI: доказательство открыто на GitHub

OpenAI объявила это 8 сентября 2026. Считала не публичная модель, а внутренняя, доступа к ней нет ни у кого.

Верить на слово не требуется. Доказательство формализовано в Lean: эта система либо принимает вывод целиком, либо просто не собирается.

Формально закрыты альтернативы (C) и (D) официальной формулировки Clay. При любой положительной вязкости находятся гладкие начальные данные и гладкое форсирование, при которых гладкого решения на всё время нет. Простыми словами, течение в уравнении разгоняется до бесконечной скорости за конечное время. Тем же репозиторием закрыт второй случай, уравнение Euler вообще без форсирования.

Проверить может любой. Репозиторий github.com/openai/NavierStokesAndEuler лежит открытым под лицензией Apache-2.0. Нужен Lean 4.34.0-rc2 с Mathlib и Lake, ставится через elan, сборка идёт двумя командами: `lake exe cache get` и `lake build`. Для независимой проверки в репозитории есть отдельный раздел ComparatorChallenges.

Прогон вышел дорогим. На Navier–Stokes ушло 2,7 млн сообщений между агентами и 130 млрд выходных токенов, на все задачи вместе 4,9 млн сообщений и около 300 млрд токенов. По публичным ценам API это примерно 15 млн долларов за один результат, посчитал Simon Willison.

Раньше к этому шли руками. Tristan Buckmaster из NYU и Levent Alpöge из Anthropic вели ту же программу около года на личной договорённости, без институциональных соглашений. Прорыв у них случился 15 августа 2026, проверка в Lean прошла 22 августа. Работали они тоже с моделями: Claude, Codex на GPT-5.6 Sol, позже Astra для текстов и аудита аргументов.

Terence Tao 7 сентября разобрал три их препринта и зафиксировал, что полный Navier–Stokes с гладким форсированием и Euler без форсирования на тот день оставались открытыми. Объявление OpenAI пришло на следующие сутки.

Buckmaster рассказывает, что на звонке 6 сентября Sébastien Bubeck описал ему стостраничное доказательство, сделанное почти без человеческого участия. По ходу разговора выяснилось, что работала целая команда и что даже показанный ему промпт написан через Codex, а первый промпт ушёл лишь за несколько дней до этого, уже после того как информация об их работе дошла до OpenAI. На вопрос, училась ли модель на их сессиях в Codex, ответа он не получил.

К качеству машинного текста Buckmaster относится трезво. Первое доказательство от LLM он называет самым чудовищным, что читал в жизни, а собственный текст по Euler описывает словами AI slop. Главное в событии он видит в другом: математик с моделью делает такую работу за месяц, и это он называет моментом Deep Blue против Каспарова.

Миллиона не будет. По правилам Clay Mathematics Institute от 26 сентября 2018 институт не принимает прямые заявки на премию. Её рассматривают только при трёх условиях сразу: публикация в квалифицирующем рецензируемом издании, минимум два года после неё и признание мировым математическим сообществом.

Публикации в рецензируемом журнале пока нет, а двухлетний отсчёт Clay начинается только после неё.