Входит ли математика в консерваторию?

Когда доказательства идут в машину

На той же неделе, когда Claude завершил формализацию доказательства Великой теоремы Ферма на языке Lean, в почте обнаружилась препринт с названием The Spherical Hadwiger Theorem. Гипотеза о сферической теореме Адвигера¹, открытая с 1974 года, описывает нишевый, но важный инструмент интегральной геометрии. На детали гипотезы здесь не будем заостряться; заинтересованным можно посмотреть предыдущую заметку, где эта теорема (тогда ещё гипотеза²) заметно упрощала доказательство одной небольшой леммы.

Суть же вот в чём: новый препринт авторов Ван и Ву из Хунаньского университета, похоже, доказывает гипотезу с помощью ИИ. В заключительном разделе приведён такой отказ от ответственности:

Во время подготовки этого рукописи OpenAI Codex использовался для помощи в разработке деталей доказательства, выявлении пробелов и моментов, требующих уточнения, организации и форматировании рукописи, а также редактировании английского текста. Авторы проверили и верифицировали весь содержащий ИИ-помощь математический материал и предложенные изменения, приняли все окончательные математические и редакционные решения и берут на себя полную ответственность за рукопись.

Этот отказ оставляет открытым вопрос: выполнил ли Codex значительную часть работы, которая до недавнего времени требовала квалификации исследователя-математика — разработку деталей доказательства³, поиск и исправление пробелов, а возможно и написание самой статьи. Кроме того, работа отличается полировкой и удобочитаемостью (для исследователя в этой области).

Следует оговориться: полной верификации доказательства не проводилось; оно прошло проверку здравым смыслом вместе с Claude и выглядит логичным, но полное усвоение потребует больше времени. Это не критика авторов — похоже, очень хорошая работа, стоящая внимательного изучения. Они даже следовали всем принципам использования ИИ, изложенным в Leiden Declaration.

Вехе́, близко к сердцу

Доказательство сферической теоремы Адвигера — это личное. Попытка доказать её была ещё в аспирантуре, и в этом году даже предпринял половинчатую попытку с помощью ИИ. Это не теорема из заголовков газет, но это не спасло её.

Такой исход неудивителен. Когда выпустили GPT-4, OpenAI опубликовала отчёт о влиянии LLM на рынок труда. Воздействие ИИ на работу математиков оказалось наивысшим из всех категорий в модели; белая книга оценила, что 100% работы математика подвергается воздействию LLM по трём различным моделям. Выше, чем для писателей, переводчиков, художников и дизайнеров. Разница только в том, что математикам потребовалось чуть больше времени, чтобы ощутить боль.

Искушение назвать задержку доминирования LLM в математике проявлением её сложности было бы отчасти самонадеянно. Подозреваю, что задержка связана скорее с тем, что исследовательская математика имеет меньше экономической ценности — и меньше данных для обучения — чем эти другие творческие области.

Пора в консерваторию?

Возьмём классическую музыку. Наше общество не поддерживает классических музыкантов так же, как популярных исполнителей. Классическая музыка институциализирована, отправлена в консерваторию как реликвия. Небольшая часть общества решила, что способность исполнять её стоит сохранения, и выделяет каплю капитала на это: обучение молодёжи, зарплаты нескольким лучшим исполнителям в крупнейших городах.

Мог бы такой модель сработать для математиков? Легко себе представить: во времена Евклида математика была в основном интеллектуальным занятием для немногих склонных людей. Математическая консерватория могла бы помочь математике развиваться даже когда создание новых результатов станет нетрудным, а трудным будет понимание и объяснение их значения.

Но чистая математика уже находится в консерватории, известной как академия. Вне университета рабочие места для чистых математиков редки. Результаты понимают только избранные. Имеет ли значение, что все сложные результаты вскоре будут доказаны компьютерами?

Итоговые размышления

Стоит поддерживать людей, продолжающих культурное дело, которое сейчас зовётся «исследовательской математикой». Математика, особенно чистая, всегда была рассказыванием историй, помогающих нам глубже понимать реальность. Через упрощение и абстрагирование мы начинаем видеть скрытую структуру: параллельные прямые никогда не пересекаются, сфера выглядит одинаково в любом направлении, простых чисел бесконечно много. Но нынешние системы поддержки математиков, как и многих других творческих областей, нуждаются в кардинальных изменениях для адаптации к новым реальностям ИИ.

Структуры стимулов, поддерживающие эту работу, неудачно приспособлены к тому, что приносит ИИ. Эти инструменты затрудняют проверку корректности даже сложного аргумента, не говоря уж о том, кто заслуживает финансирования, учёного звания и славы. Перед нами стоит выбор: как сделать людей значимыми, когда их интеллектуальный труд просто не сравнится с компьютерами? Когда интеллект ограничен лишь кремнием и электричеством, будем ли мы готовы поддерживать культуру, в которой существуют математики? Я очень надеюсь, что да.