19 сентября 2026 г.
Математики не могут отказаться от ИИ: OpenAI получила решение Navier-Stokes за 88 часов
8 сентября OpenAI заявила, что её внутренняя модель создала аналитическое доказательство возникновения сингулярности уравнений Navier-Stokes за конечное время. Решение получили примерно за 88 часов, Lean-проверка заняла ещё 17 часов. Агенты отправили 2,7 млн сообщений и использовали около 130 млрд output tokens.
WIRED описывает конфликт: ИИ создаёт экзистенциальный риск для математики, но исследователи продолжают пользоваться им из-за практической пользы.
Рабочий компромисс. Тристан Бакмастер работал над задачей с Codex и Claude. После конфликта с OpenAI он продолжил использовать Codex для редактирования исследовательских статей и разбора логических шагов доказательства. Расследование OpenAI от 8 сентября подтвердило, что его промпты, отправленные за 2 месяца до публикации, не могли повлиять на результат, включая обучение, а его работа с Levent Alpöge существенно отличалась от работы OpenAI.
Репродуцируемый слой. OpenAI опубликовала в GitHub Lean 4-формализации результатов по Navier-Stokes и Euler. Для сборки нужны Lean 4.34.0-rc2, Mathlib и Lake, после чего выполняются `lake exe cache get` и `lake build`.
Это уже серия. WIRED сообщила, что Anthropic использовала Claude для доказательства 29 500 малых теорем и формализации существующего доказательства теоремы Ферма. OpenAI в августе заявила о прогрессе по 10 давним математическим задачам.
Доступ расширяют. ChatGPT for Academic Researchers должна дать 100 000 исследователей бесплатный доступ к frontier-моделям к 2027 году. Стартовая когорта составляет 10 000 человек, а одобренное рабочее пространство включает до 5 бесплатных мест на 12 месяцев. Для заявки нужны статус research faculty или postdoctoral researcher, учреждение из списка, статья за последние 3 года и проверка через SheerID.
Возражения остаются. Более 4 000 человек подписали Leiden Declaration, 25 лауреатов Fields Medal присоединились к открытому письму, а более 2 000 связанных с Caltech людей призвали приостановить AI-математический хакатон.
К 2027 году OpenAI планирует довести бесплатный доступ к frontier-моделям до 100 000 исследователей.
Первоисточник
