Доказательства ИИ можно проверять как код: OpenAI выложила результат по Navier–Stokes

Поиск и проверка. По данным компании от 8 сентября, около 10 000 ИИ-агентов искали решение задачи о движении жидкости. Они получили доказательство образования сингулярности при гладкой внешней силе: скорость в математической модели становится бесконечной за конечное время. OpenAI использовала внутреннюю модель, которую называет значительно способнее GPT-6 Astra.

Математики тоже работали с агентами. По данным Саймона Уиллисона, Тристан Бакмастер и Левент Альпёге почти год исследовали связанную задачу с Claude и Codex и получили прорыв 15 августа. Бакмастер затем публично оспорил действия OpenAI.

Результат бывает частичным. До исследования Anthropic математики доказали, что на критической прямой лежат как минимум 41,6% интересующих их нулей дзета-функции. В результате, опубликованном 10 августа, исследовательская версия Claude подняла эту границу до 67,2%, не доказав саму гипотезу Римана. Сотрудник Anthropic Джарред Самнер получил результат за 2 сессии Claude Code: после 650 неудачных идей модель координировала около 60 субагентов.

Для практика здесь есть знакомый рабочий процесс: агент ищет решение, отдельный инструмент проверяет результат. Lean проверяет формальное доказательство по правилам логики. Код доказательств Navier–Stokes и Euler доступен в openai/NavierStokesAndEuler: после установки elan в каталоге проекта выполняются `lake exe cache get` и `lake build`. Проект требует Lean 4.34.0-rc2.

Первоисточники: [The Verge разбирает споры вокруг математических результатов ИИ](https://www.theverge.com/ai-artificial-intelligence/1004933/ai-math-openai-breakthrough-solution). OpenAI описывает [поиск и проверку результата Navier–Stokes](https://openai.com/index/navier-stokes-solution/) и публикует [код для сборки доказательств](https://github.com/openai/NavierStokesAndEuler). Anthropic описывает [результат Claude по дзета-функции](https://www.anthropic.com/research/riemann-zeta).

6 октября OpenAI опубликовала в openai/math 722 рукописи в 372 семействах с PDF, исходниками и Lean-доказательствами для части результатов.