ИССЛЕДОВАНИЕ · RESEARCH · #1806
OpenAI опубликовала 719 AI‑сгенерированных математических рукописей; математики предупреждают, что проверка займет годы
OpenAI выложила на GitHub репозиторий из 719 рукописей с почти 400 AI‑сгенерированными математическими результатами по множеству дисциплин; компания заявила, что около 300 основных результатов (≈42%) формализованы и планирует добавлять ещё формализации. Математики в беседах с The Verge отметили, что объём и неравномерное качество верификации — формализации в Lean есть не для всех и разного качества — потребуют годами коллективной проверки.
КЛЮЧЕВЫЕ ТЕЗИСЫ
- OpenAI выложила на GitHub репозиторий из 719 рукописей с почти 400 AI‑сгенерированными математическими результатами по множеству дисциплин; компания заявила, что около 300 основных результатов (≈42%) формализованы и планирует добавлять ещё формализации.
- Математики в беседах с The Verge отметили, что объём и неравномерное качество верификации — формализации в Lean есть не для всех и разного качества — потребуют годами коллективной проверки.
- Масштаб релиза и неравномерная формальная верификация могут изменить практики создания и проверки математических результатов и переложить серьёзную нагрузку по верификации на научное сообщество.
БРИФ ДЛЯ РЕШЕНИЙ
УВЕРЕННОСТЬ
ЧТО ИЗМЕНИЛОСЬ
OpenAI выложила на GitHub большой репозиторий из 719 рукописей, содержащих почти 400 AI‑сгенерированных математических результатов в разных подполях; в релизе есть отдельные формализации в Lean и небольшое число раскрытий цепочки рассуждений модели.
ПОЧЕМУ СЕЙЧАС
Объём релиза и неравномерная формальная верификация создают немедленную и большую нагрузку на математическое сообщество и ставят вопросы о том, как результаты, сгенерированные ИИ, будут верифицироваться и интегрироваться в исследовательскую практику.
КОГО ЗАТРАГИВАЕТ
Непосредственно затронуты математики и исследователи во многих подполях (комбинаторика, геометрия, теория чисел, теоретическая информатика, алгебра, топология, теория вероятностей, статистическая механика, математическая физика), широкое математическое сообщество, которое должно оценивать и формализовать результаты, а также консультативные органы вроде AGMAI.
ПОДТВЕРЖДЕНО
- OpenAI опубликовала 719 рукописей на GitHub. (TechCrunch) - В репозитории содержатся почти 400 AI‑сгенерированных математических результатов, распределённых по более чем 700 рукописям. (The Verge) - Некоторые рукописи содержат формализации в инструментарии Lean; эти формализации использовались для оценки некоторых утверждений. (The Verge) - Только в 10 из 719 рукописей были опубликованы цепочки рассуждений модели. (TechCrunch) - Консультативная группа по математике и ИИ (AGMAI) выпустила рекомендации и призвала лаборатории прекратить тестирование сложных математических задач на закрытых моделях; AGMAI также заявила, что оценка исполнения рекомендаций остаётся за математическим сообществом. (TechCrunch) - Математики, с которыми разговаривали журналисты, описали объём как ошеломляющий и говорили, что разбор и верификация могут занять годы. (The Verge)
НЕОПРЕДЕЛЁННОСТЬ
- Точное число и процент результатов, которые формально верифицированы (источники дают противоречивые/частичные формулировки о наличии формализаций). (TechCrunch; The Verge) - Полнота, корректность и качество формализаций в Lean по всем рукописям (в отрывках говорится, что степень верификации «сильно различается», но нет перечисления верифицированных результатов). (The Verge) - Какие конкретные результаты подтверждены независимой верификацией сообществом помимо отдельных формализаций. (в отрывках нет явных данных) - Будет ли OpenAI финансировать или иным образом поддерживать масштабную проверку людей, и будет ли оно публиковать больше цепочек рассуждений или дополнительных формализаций. (TechCrunch отмечает рекомендацию AGMAI финансировать работу, но ответ OpenAI или обязательства не приведены; AGMAI не дала развёрнутой оценки по запросу). (TechCrunch) - Конкретные сроки оценки сообществом; источники передают экспертные оценки о том, что это может занять годы, но не дают системного графика. (The Verge) Метка для отсутствующих/конфликтующих данных: подсчёты и проценты формализованных/верифицированных результатов противоречивы или не полностью раскрыты в приведённых выдержках. (TechCrunch; The Verge)
ЧТО ОТСЛЕЖИВАТЬ
Конкретные наблюдаемые сигналы для отслеживания - Обновления репозитория на GitHub: новые или расширенные формализации в Lean; увеличение числа рукописей с опубликованными цепочками рассуждений модели (текущее число = 10). (TechCrunch; The Verge) - Публичные заявления или развёрнутая оценка от AGMAI или других консультативных органов о том, соблюдала ли OpenAI рекомендации AGMAI. (TechCrunch) - Уведомления об независимой верификации сообществом: опубликованные подтверждения, принятые Lean‑доказательства или публичные отказы/исправления для конкретных рукописей. (The Verge) - Коммуникации OpenAI о поддержке верификации (финансирование, партнёрства или инфраструктура) либо дополнительные релизы данных/документации по доказательствам. (TechCrunch) - Признаки нагрузки сообщества: организованные проекты по верификации (репозитории, вики‑трекинг, спринты формализации) и отчёты исследовательских групп о пройденных объёмах работ и сроках. (The Verge)
ПОЧЕМУ ЭТО ВАЖНО
Масштаб релиза и неравномерная формальная верификация могут изменить практики создания и проверки математических результатов и переложить серьёзную нагрузку по верификации на научное сообщество.
КАРТА ДОКАЗАТЕЛЬСТВ
4Редакционные тезисы связаны с конкретными источниками. Отдельно отмечены подтверждения, противоречия и контекст.
OpenAI опубликовала большой набор рукописей — 719 рукописей с почти 400 AI‑сгенерированными математическими результатами по множеству разделов математики.
ПОДТВЕРЖДЕНОПроверено 2026-10-09 · 2 подтверждений
TechCrunch говорит о сотнях опубликованных решений и в отрывке прямо упоминает 719 рукописей.
ПОДТВЕРЖДАЕТ The Verge AIMEDIA · 2026-10-09The Verge указывает на почти 400 AI‑результатов, распределённых более чем по 700 рукописям, и на множество покрытых разделов.
Некоторые рукописи содержат формализации в системе Lean, но формализованы только отдельные работы, и качество/полезность формализаций неоднородны.
ПОДТВЕРЖДЕНОПроверено 2026-10-09 · 1 подтверждений
The Verge указывает, что формализации в Lean «вкраплены» в сотни рукописей и что они помогали в оценке претензий ранее.
КОНТЕКСТ TechCrunch AIMEDIA · 2026-10-09TechCrunch передаёт, что математики рекомендовали формализации для непонятных доказательств, то есть формализация рассматривается как ответ на неоднородность ясности доказательств.
Только десять из 719 рукописей включали публикацию цепочки рассуждений модели (следов внутреннего вывода), согласно TechCrunch.
ПОДТВЕРЖДЕНОПроверено 2026-10-09 · 1 подтверждений
Математики в беседах с The Verge сказали, что понимание и верификация содержания публикации могут занять годы и, вероятно, потребуют значительных усилий сообщества.
ПОДТВЕРЖДЕНОПроверено 2026-10-09 · 1 подтверждений
The Verge цитирует многих математиков, называвших релиз «ошеломляющим» и отмечавших, что простое прочтение аннотаций занимает много времени; указывается мнение, что разбор займет годы.
КОНТЕКСТ TechCrunch AIMEDIA · 2026-10-09TechCrunch сообщает, что AGMAI рекомендовала OpenAI помочь финансировать работу людей по осмыслению результатов, что даёт контекст необходимости человеческих усилий.
ИСТОЧНИКИ И ХРОНОЛОГИЯ
2When OpenAI released hundreds of claimed solutions to some of the world’s hardest math problems this week, the frontier lab said that it had consulted an advisory group of elite mathematicians to avoid the controversy that came with the last time one of its models solved a long-standing problem in the field. But OpenAI fell short of those standards, particularly where the mathematicians emphasized the need for human…
Careers upended overnight, academics will have to separate solutions from slop while OpenAI moves on. “Staggering.” “Overwhelming.” “Unprecedented.” “Surreal.” “Pure insanity.” Those were among the descriptions more than three dozen mathematicians reached for in conversations with The Verge as they tried to make sense of the flood of mathematical results OpenAI abruptly dropped on the field this week. Amid the awe,…