![](data:image/svg+xml;charset=utf-8,<svg width="640" height="640" style="background-color:%2344badc;font-family:Nunito,sans-serif" viewBox="0 0 100 100" preserveAspectRatio="xMidYMid meet" xmlns="http://www.w3.org/2000/svg">
<text font-size="30" x="50%" y="50%" dy="5" fill="white" dominant-baseline="middle" text-anchor="middle">fl</text>
</svg>)
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
Доклад пройдет в зуме по ссылке.
Спикер: Василий Ильин, Директор Лаборатории ИИ для Математики в Университете Вашингтона
Тема доклада: ИИ для формализации математики: прогресс за 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
Доклад пройдет в зуме по ссылке.