Lecture-invitation to the seminar «Mathematics in Lean 3 and Neural Theorem Proving» by Fedor Pavutnitskiy
Fedor Pavutnitskiy will give a lecture-invitation to the seminar «Mathematics in Lean 3 and Neural Theorem Proving» on February 17 at 19.00
In this semester I would like to get to know the formal theorem proving language Lean 3. In particular, I would like to understand how Lean is applicable in contemporary mathematics, apart from the type theory and verification questions. In the first part of the lecture, I will talk about my personal impressions of Lean and give an overview of the language to the extent that I managed to get to know it myself. In the second part, we will look into the future and try to understand how the synthesis of interactive theorem provers and modern machine learning can change and expand our “classical” proof process. I will give examples of recent papers in this area. During the lecture some auxiliary relevant topics will be mentioned, it would be interesting to discuss them at the upcoming seminar.
More information about the seminar and registration: https://indico.eimi.ru/event/877/.
Everyone is welcome!
_________________________________________________________________________
17 февраля в 19.00 Федор Павутницкий прочитает лекцию-приглашение на семинар «Mathematics in Lean 3 and Neural Theorem Proving»
В этом семестре хочется начать знакомство с языком формального доказательства теорем Lean 3. В частности, хочется понять, насколько Lean применим в современной математике, вне теории типов и вопросов верификации. В первой части лекции я расскажу о личных впечатлениях от Lean 3 и дам обзор языка в том объеме, в котором успел с ним познакомиться сам. Во второй части мы устремимся в будущее и попробуем понять, насколько синтез подобных interactive theorem prover’ов и современного машинного обучения может изменить и расширить наш «классический» процесс доказательства. Я приведу примеры недавних работ, в которых делаются первые шаги на этом пути. По ходу лекции также будут обозначаться вспомогательные темы, которых было бы интересно коснуться на предстоящем семинаре.
Более подробная информация о семинаре и регистрация: https://indico.eimi.ru/event/877/.
Приглашаются все желающие!
_________________________________________________________________________