08.09.2025

Математика в режиме ИИ: человек, машина, доказательство

Андрей Окуньков на факультете математики ВШЭ

Аннотация:

Как искусственный интеллект влияет на саму природу математического открытия? В рамках этого мероприятия лауреат премии Филдса Андрей Окуньков предложит критический взгляд на роль языковых моделей в математике, задавшись вопросом о границах «речистого разума». Его философский разбор дополнит прагматичная перспектива исследователей сотрудников научно-учебной лаборатории сложных сетей, гиперграфов и их приложений НИУ ВШЭ — Артёма Малько и Сергея Усанова.

Они расскажут, как ИИ уже помогает формулировать гипотезы, находить контрпримеры и даже открывать новые формулы — в частности, в теории узлов. От практических кейсов в Nature до интеграции LLM с системами вроде Lean и Sage — докладчики покажут, как ИИ становится не просто инструментом, а активным участником математического поиска. Мероприятие объединит глубокие идеи, свежие результаты и вызовы будущего математики.

23-го сентября на факультете математики ВШЭ

Программа: 

16:00-16:50 Андрей Окуньков — «Критика речистого разума»
Речь пойдет о языке математики и той роли, которую языковые модели уже играют или могут сыграть в том, как профессионалы и любители с языком математики взаимодействуют. Не являясь ни специалистом по большим языковым моделям, ни их активным пользователем, докладчик не планирует глубокого и систематического освещения данной темы. Скорее, речь пойдет о некоторых простых принципах и примерах.

17:00-17:50  «Новый инструмент науки: как использовать ИИ в математике»
17:00-17:20 Сергей Усанов 
Машинное обучение стремительно проникает в повседневную жизнь, решая всё больше прикладных задач. Более того, в последнее время оказалось, что искусственный интеллект можно успешно применять и в чистой науке!
В своём докладе я расскажу, на какой идее зиждиться машинное обучение, и про то, как оно помогло открыть новую формулу в теории узлов.

Мой рассказ будет разбит на три логических блока:

  1. Что такое узлы, как их различать и как упрощать?
  2. Как выглядит самая обученная модель и как все остальные модели её приближают?
  3. Как подружить машинное обучение и чистую математику? (и что у нас из этого получилось)

17:30-17:50 Артем Малько 
Доклад посвящён тому, как большие языковые модели уже помогают математику -- от помощи с гипотезами и поиска контрпримеров до автоматизации повседневных исследовательских задач. Я коротко разберу несколько показательных кейсов из недавних работ (Nature по наводке гипотез в теории узлов, RL-подход к задачам типа Эндрюса-Кертиса, FunSearch/PatternBoost для поиска нетривиальных конструкций) и затем обсудим индустриальные тренды 2025 года: пост-тренировочные методы (RLVR), улучшение рассуждений и агентные циклы с вызовом инструментов. Ключевой вывод: масштабируемые методы поиска и обучения дают новые рычаги к старым открытым проблемам; практическая польза приходит от системной интеграции LLM-агентов с GAP/Sage/Lean и доступного вычислительного бюджета.