Select Page

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/.

Приглашаются все желающие!

_________________________________________________________________________

Receive news updates

Subscribe to receive actual news updates

Thank you for subscription

Confirm your subscription via the link that you will receive in your mailbox.