Lean lecture
NMMB568, Formal Mathematics and Proof Assistants, 2+1
Schedule
There are two parallel lectures, choose one that suits you.
- Malá Strana SW1: Tuesday 9:00 – 10:30 (lecture), 10:40 – 11:20 (exercise / consultation)
- or Karlín K4: Wednesday 17:20 – 18:50 (lecture), 19:00 – 19:40 (exercise / consultation)
Links
Lectures
I am following my write-up notes here in the directory LeanTeaching. The actual files shown in the lectures are stored in the directory Live.
- Lean as a basic functional language: Numbers, top-bottom type inference, functions, recursion, structures, object-oriented syntax, inductive types
- Dependent types, Pi & Sigma types, Vector implementations, Curry-Howard correspondence (Propositions as Types), inductive type vs. proposition (examples Or & Exists).
- Forward & backward proof, basic tactics (refine, exact, intro, apply), practical example (tactics induction, rw, rw??), library search
Homework
Enroll in the owl submission system via this link. You need 60 points from homeworks to get the credit.
- Extending numerical Expr data type. [Lean file]
- Implementing dependent zeros function, and writing explicit proof terms. [Lean file]
- Proving identity about LCM & proving correntness of Expr.deriv [Lean file]
Project / Exam
To get an exam, you must do a Lean project, which we will discuss at the exam. Formalizing your favorite math problem(s), theorem, topic, algorithm... We can discuss proposals individually. It is possible that I will put some suggestions here as well (but do not count on it).
Other info
Go back to the promo page.