Mathematics in Lean 3 and Neural Theorem Proving
by Fedor Pavutnitskiy
The seminar is for those interested in the role of interactive theorem provers (ITP) in contemporary mathematics, as well as those interested in code generation.
Lean 3 is a formal theorem proving language that turns the proving process into a computer game. Its mathematical library is constantly expanding and includes more and more statements from modern mathematics. Our goal is first to enjoy the process of formalisation (this is quite real), and second to realise that formalisation allows us to expand our thinking, for example, with deep models that generate theorems (this is quite unreal).
Our time will be spent on:
1. Learning Lean 3 using existing repositories like formalising-mathematics.
2. Studying papers on the applications of machine learning to automatic proofs.
The seminar will be practice-oriented, any degree of involvement is welcome, from free interest in formal methods, to mathlib commits and your own code-generating models. In case you are interested in other languages, like Coq, other axiomatics, like homotopy type theory, all these topics are also within the scope of the seminar.
Everyone is welcome! Registration is required.
Семинар для интересующихся применением интерактивных средств доказательства теорем в современной математике, а также интересующихся вопросами генерации кода.
Lean 3 — это язык формального доказательства теорем, превращающий процесс доказательства в компьютерную игру. Его математическая библиотека mathlib постоянно расширяется и включает в себя все больше утверждений из современной нам математики. Наша цель — сначала получить удовольствие от процесса формализации (это реально), а затем осознать, что формализация позволяет расширить наше мышление, например, с помощью глубоких моделей, которые генерируют теоремы вместе с нами (это фантастично).
У нас будет два основных направления:
1. Будем вместе учить Lean 3 на примере существующих репозиториев вроде formalising-mathematics.
2. Будем разбирать статьи о применениях машинного обучения в автоматических доказательствах.
Семинар будет проходить почти полностью в практическом ключе, любая степень вовлеченности приветствуется: от свободного интереса к формальным методам, до коммитов в mathlib и собственных генерирующих код моделей. Если вам интересны другие языки, вроде Coq, другие аксиоматики, вроде гомотопической теории типов, то все это возможно и обсуждаемо.
Приглашаются все желающие! Необходима регистрация.
