Lean at Matfyz

The Teacher

Hi, I am Mirek Olšák. I got my Ph.D. here at Matfyz 7 years ago, then did research abroad on AI for math from different angles. For the last two years, I worked in Cambridge & Google DeepMind with several Lean experts, and got to understand Lean well.

Lean

Official website

Lean is a language used to state mathematical theorems and verify their proofs. Its foundations of dependent type theory allow for arbitrarily abstract mathematical constructs.
Lean is also a programming language (same broad family as Haskell). Lean's own compiler is written in the very same language.
Lean is becoming popular. Mathematicians as well as AI companies are getting interested.

The Course

NMMB568, Formal Mathematics and Proof Assistants, 2+1
Time will be decided in the scheduling system of the Department of Algebra.
Materials: here
Lectures will be more theoretical than a TeX / C++ course but less theoretical than a math course, or a course on functional programming.
- We will look at deep aspects of the language, to let the students understand something under the hood.
- We will be directly interacting with Lean basically all the time.
To get an exam, you will do a project in Lean of an appropriate difficulty.
Exercises are to assist you playing with Lean. You can work there on the lecture homeworks or the main project.
Homeworks are relatively easy to help you get to understand one concept at a time
- data structures
- curry-howard correspondence
- basic proofs
- equality kinds
- type classes
- relationship to ZFC foundations
- proving termination

Q & A

Q: How does it relate to courses by Martin Suda or Robert Šámal? A: I am taking the course after Martin Suda, but I plan to do it a bit in my own way. To my understanding, R. Šámal is focusing on specific examples of how to do math in Lean; I would like to look at more general aspects of the language.
Q: What do I need to know? What are the prerequisites? A: Basic knowledge of the following domains helps:
- Functional programming
- Mathematical Logic & Set theory
None of it is strictly speaking necessary, but if you have no idea about any of that, it might be a bit challenging for you.
Q: All of this is in English, is the course going to be in English too? A: Expect English; the course materials will be in English. On the other hand, if only Czech & Slovak students sign up, I can switch to Czech too.
Q: Come on, this promo looks a bit far-fetched, do you really believe this is the language of the future? A: I do, but I also think we should pursue that as the better option. The other option is tons of math & code generated by language models without any proper guarantees.
Q: Are there also other formal languages besides Lean? A: Sure, as well as there are multiple programming languages, there are multiple formal languages, such as Isabelle, HOL, Rocq (former Coq), Agda, Mizar, Metamath, TPTP, SMT-Lib, ... I have decided to focus on Lean because it is currently getting some traction, and I know Lean the best out of these languages. There is also a course on Isabelle at Matfyz by Štěpán Holub, and on SAT & SMT solvers by Mikoláš Janota.