Исследователи размышляют о будущем математики в условиях активного развития искусственного интеллекта. Теренс Тао из Калифорнийского университета в Лос‑Анджелесе полагает, что ИИ может открыть эру «большой математики», в которой люди и машины будут вместе решать сложные задачи.
Автор текста, Питер Адамс, вспоминает свои годы работы над докторской степенью по прикладной математике — его исследования касались моделирования взаимодействия световых волн в жидких кристаллах. Сейчас он думает, что с помощью ИИ его работа могла бы быть выполнена за несколько часов или дней. При этом он осознаёт ценность многолетнего труда коллег, занимавшихся чистой математикой: для них радость заключалась в долгом пути к пониманию.
Математики на протяжении веков замечают связи и закономерности, строят гипотезы и с помощью логики доказывают или опровергают их. Этот процесс требует времени и вдумчивой работы. Однако современные системы ИИ начинают действовать в обход этого медленного процесса.
Роль вычислений в продвижении математики известна уже несколько десятилетий: например, 50 лет назад с помощью компьютера была доказана теорема о четырёх цветах. Но до недавнего времени человек по‑прежнему играл центральную роль — выдвигал гипотезы, разрабатывал стратегии их подтверждения, проверял доказательства.
Сейчас ИИ бросает вызов устоявшемуся порядку. За несколько лет большие языковые модели превратились из простых инструментов в продвинутые системы математического мышления. Летом системы Google DeepMind и OpenAI достигли уровня самых одарённых старшеклассников и завоевали золотую медаль на Международной математической олимпиаде.
Система Google DeepMind Aletheia недавно самостоятельно подготовила результаты исследований, которые могут быть опубликованы на уровне докторской диссертации. А новая система ИИ от OpenAI опровергла важную гипотезу в комбинаторной геометрии — это достижение ведущие математики назвали важной вехой в развитии ИИ в математике.
Кроме того, происходит интеграция больших языковых моделей с инструментами для проверки математических доказательств (например, Isabelle, Lean и Rocq). Раньше математикам приходилось вручную переводить свои доказательства в машиночитаемый формат, теперь же этот процесс начинают автоматизировать. Например, логический агент Gauss от компании Math, Inc. помог формализовать доказательство, за которое математик Марина Вязовская получила медаль Филдса в 2022 году: сначала он ускорил работу специалистов над 8‑мерной задачей, а затем самостоятельно справился с более сложным 24‑мерным случаем за две недели.
Эти достижения показывают, что ИИ уже способен решать задачи, которые раньше считались прерогативой человека. По мере развития технологий значительная часть рутинной работы математиков может перейти к машинам.
