OpenAI Codex помог доказать 50-летнюю гипотезу Хадвигера
Блогер-математик рассказывает, что в ту же неделю, когда Claude завершила формализацию доказательства Великой теоремы Ферма в Lean, ему на почту пришёл препринт «The Spherical Hadwiger Theorem», работа Ван и Ву из Хунаньского университета, доказывающая сферическую гипотезу Хадвигера, остававшуюся открытой примерно с 1974 года. Это нишевая, но важная задача интегральной геометрии; сам автор поста в своё время пытался доказать её ещё в аспирантуре, а позже сделал ещё одну попытку с помощью ИИ.
В заключительном разделе препринта стоит дисклеймер: при подготовке рукописи авторы использовали OpenAI Codex, чтобы прорабатывать детали доказательства, находить пробелы и места, требующие уточнения, организовывать и вёрстать текст, а также редактировать английский язык; при этом они утверждают, что сами проверили весь ИИ-контент, приняли все итоговые математические и редакторские решения и несут полную ответственность за рукопись.
Автор поста отмечает, что формулировка дисклеймера оставляет открытым вопрос, насколько большую часть работы, прежде требовавшей исследователя высокого уровня, фактически выполнил Codex: проработку деталей доказательства, поиск и устранение пробелов, а по сути и написание самого текста. По его оценке, работа получилась очень отточенной и читаемой (для исследователя в этой области). Сам он полностью доказательство не проверял, но прогнал его через Claude Fable, оно прошло «проверку на нюх», хотя для полной проверки у него пока нет ни времени, ни сил. Автор подчёркивает, что это не упрёк Ван и Ву: препринт выглядит как хорошая работа, а его авторы, по его словам, соблюли все принципы использования ИИ из Лейденской декларации.
Далее автор переходит к более широкому тезису: он напоминает, что ещё в эпоху GPT-4 OpenAI выпустила отчёт о влиянии ИИ на рынок труда, в котором уязвимость профессии математика к автоматизации языковыми моделями была оценена в 100%, по всем трём использованным в отчёте моделям труда, и выше, чем у писателей, переводчиков, художников и графических дизайнеров. Тогда этот прогноз не сбывался быстро, по мнению автора, не потому что исследовательская математика особенно сложна, а скорее потому, что у неё меньше экономической ценности и меньше обучающих данных, чем у других творческих областей.
Автор проводит параллель с классической музыкой, которая давно институционализирована и превращена в своего рода «консерваторию»: общество выделяет отдельный ресурс на сохранение этого занятия, а не поддерживает его через рынок напрямую. Он задаётся вопросом, не ждёт ли исследовательская математика та же судьба, при том что, по его наблюдению, чистая математика по сути уже находится в такой «консерватории», только называется университетской академией, а вакансий вне неё для чистых математиков и так немного. Вывод автора: стоит продолжать поддерживать исследовательскую математику как культурное занятие, но нынешние системы поддержки, гранты, репутация, штатные позиции, плохо приспособлены к тому, что несёт с собой ИИ, особенно когда становится труднее оценить, кто на самом деле сделал сложную работу и кто заслуживает финансирования и признания.
Ключевые факты
- Математики Ван и Ву (Хунаньский университет) опубликовали препринт с доказательством сферической гипотезы Хадвигера, открытой примерно с 1974 года.
- В дисклеймере препринта сказано, что OpenAI Codex помогал прорабатывать детали доказательства, находить пробелы, оформлять рукопись и редактировать английский текст; авторы утверждают, что сами проверили весь ИИ-контент и несут полную ответственность за работу.
- Автор блога, математик, ранее сам пытавшийся доказать эту теорему, прогнал доказательство через Claude Fable: оно прошло «проверку на нюх», но полностью автор его не верифицировал.
- Отчёт OpenAI эпохи GPT-4 о влиянии ИИ на рынок труда оценивал уязвимость профессии математика в 100% по всем трём использованным моделям труда, выше, чем у писателей, переводчиков, художников и графических дизайнеров.
- Автор сравнивает возможное будущее исследовательской математики с судьбой классической музыки, институционализированной в консерваториях, и указывает, что чистая математика уже во многом существует в похожем режиме, в виде университетской академии.
Почему это важно
Препринт Ван и Ву, конкретный пример того, что ИИ-инструмент вроде OpenAI Codex по заявлению самих авторов участвовал в проработке доказательства полувековой открытой математической гипотезы, а не только в оформлении текста. Это подаётся как веха: работа, которая ещё недавно требовала исследователя высокого уровня, теперь делается с существенной помощью ИИ, и это подталкивает автора поста к более широкому разговору о будущем самой профессии математика-исследователя.
Кому это важно
Прежде всего, исследовательским математикам и университетам: именно их работа, по прогнозу отчёта OpenAI эпохи GPT-4, оказалась наиболее уязвима к автоматизации языковыми моделями среди всех рассмотренных профессий. Также это важно для тех, кто думает о будущем интеллектуального труда в целом, и для тех, кто формирует академические нормы использования ИИ, например, авторов и сторонников Лейденской декларации.
Как это применить
Дисклеймер Ван и Ву, образец того, как прозрачно раскрывать использование ИИ в научной работе: отдельно перечислено, для каких именно задач применялся Codex (детали доказательства, поиск пробелов, вёрстка, редактура английского), и отдельно зафиксировано, что итоговую проверку и ответственность несут авторы-люди. Автор поста отмечает, что это соответствует принципам использования ИИ из Лейденской декларации, такой формат раскрытия можно рассматривать как ориентир для других научных работ.
Можно ли доверять
Автор поста, сам математик, работавший над этой же теоремой ещё в аспирантуре и знакомый с темой не понаслышке, что придаёт его оценке препринта вес. Но он прямо признаёт, что не проверил доказательство полностью: лишь прогнал его через Claude Fable и получил, что оно проходит «проверку на нюх». В источнике нет данных о том, прошёл ли препринт рецензирование или принят ли он в журнал, а также не указана точная версия модели OpenAI Codex, предположение автора про «GPT 5.6» в сноске он сам подаёт как открытый вопрос, а не факт.
Риски и подводные камни
Автор указывает на системную проблему: по мере того как ИИ берёт на себя всё больше работы уровня исследователя, становится труднее определить, верен ли сложный математический аргумент, и ещё труднее решить, кто заслуживает финансирования, штатной позиции и признания за результат. Нынешние системы поддержки исследовательской математики, гранты, репутация, карьерные треки, по мнению автора, плохо приспособлены к этой новой реальности, и без их пересмотра профессия рискует свестись к узкому «заповеднику» по аналогии с классической музыкой.
«При подготовке этой рукописи OpenAI Codex использовался для помощи в проработке деталей доказательства, выявлении пробелов и мест, требующих уточнения, организации и вёрстке рукописи, а также редактировании английского текста. Авторы проверили и верифицировали весь контент, созданный при содействии ИИ, предложили правки, приняли все итоговые математические и редакторские решения и несут полную ответственность за рукопись.»
— дисклеймер об использовании ИИ в препринте Ван и Ву, «The Spherical Hadwiger Theorem»