🧮 6 октября OpenAI открыла репозиторий с 719 рукописями, объединёнными в 372 семейства результатов. По описанию компании, большинство получено одной неопубликованной внутренней моделью: ей предложили около 4 000 открытых задач, а на один отобранный результат в среднем приходилось примерно три часа вычислений уровня ChatGPT Pro.
Это не 719 доказанных «решений великих задач». Сами OpenAI прямо предупреждают: результаты находятся на разных стадиях проверки; неформализованные утверждения могут содержать ошибки. Для 300 из 719 главных результатов — около 42% — приложены формализации в Lean, системе проверки математических доказательств. Остальные тексты ещё должны пройти обычную, медленную и независимую математическую проверку.
И проверка началась сразу. Уже 7 октября в журнале изменений появились три отозванные рукописи: ошибка знака разрушила один аргумент и два зависимых от него результата. Ещё 14 работ получили исправления доказательств, уточнения условий или переработанные зависимости; 13 дополнительных текстов обновили ссылки на эти версии.
• Это не доказательство, что модели «ничего не умеют».
• Это демонстрация нового масштаба задачи проверки: система способна генерировать математические кандидаты быстрее, чем человеческое сообщество умеет читать, проверять, объяснять и встраивать их в предмет.
Мы уже писали о двух сторонах этой проблемы: формальная проверка не гарантирует сама по себе, что формализованное утверждение точно отвечает исходной математической задаче; а верный результат ещё нужно превратить в понятную людям идею, метод и следующий вопрос. Новый выпуск OpenAI делает это различие не философским, а операционным.
⚖️ На этом фоне особенно выразительно звучит реакция Association for Human Mathematics:
Математики не просили выполнять эту работу.
У авторов есть серьёзные основания требовать аккуратности: сотни рукописей, выпущенных разом, могут перегрузить рецензирование, размыть приоритет и оставить после себя не знание, а неразобранный архив.
Но прогресс не спрашивает у профессионального сообщества разрешения, прежде чем произойти. Вопрос не в том, следовало ли моделям давать трудные открытые задачи. Их уже дали — и результаты, вместе с ошибками, оказались в публичном репозитории. Запрет на машинный поиск не вернёт прежнюю математику; он лишь оставит поле тем, кто будет искать без открытых версий, журналов исправлений и внешней критики.
Позицию AHM легко понять как защиту человеческого понимания. Но здесь есть риск перейти от защиты понимания к защите дефицита результатов. История математики не раз менялась вслед за новыми средствами: символической алгеброй, вычислительными экспериментами, компьютерными доказательствами. Они не заменили математику, а перенесли её узкое место — от рутинного счёта к постановке вопросов, проверке, объяснению и построению новых теорий.
Нужный ответ — не неолуддизм, а новая инфраструктура: больше формализации, воспроизводимые версии, автоматическая проверка зависимостей, независимый аудит, экспертный отбор и хорошее изложение. Машина может предложить тысячу доказательств; чтобы они стали математикой, нужно понять, что из этого верно, существенно и переносимо.
ИИ будет производить математические результаты всё больше и быстрее. Поэтому ближайшим узким местом становится не их получение, а проверка, отбор и включение в математическую науку как систему знания — процесс, за который пока отвечают люди.