17 августа в 20:00 MSK (19:00 CET, 10:00 PT) пройдет доклад Лаборатории формальной математики. Приглашаются все желающие.

Спикер: Василий Ильин, Директор Лаборатории ИИ для Математики в Университете Вашингтона

Тема доклада: ИИ для формализации математики: прогресс за 4 месяца

Описание: Сравним ИИ 4 месяца назад и сегодня. Насколько мы близки к формализации всей математики и как к этому подступиться? Посмотрим на эксперименты в Physlib, решение 11 новых задач в LeanEval и краудсорсинг формализации в эру ИИ. Также обсудим как мерять качество формального кода и как презентовать ИИ проект по формализации.

Материалы:
• статьи https://arxiv.org/abs/2602.05216, https://arxiv.org/abs/2606.25363
• видео https://www.youtube.com/watch?v=H2z3VRRd4aQ
• краудсорсим формализацию https://github.com/Vilin97/lean-pool

Доклад пройдет в зуме по ссылке.