Course description

Firstly, what is a proof assistant? What can a proof assistant do and what can it not do?

What a proof assistant can do:

  1. A proof assistant can verify your proof;
  2. A proof assistant can make your proof interactive (and so makes teaching/learning more engaging);
  3. A proof assistant can help you focus on one goal at a time.

What a proof assistant cannot do:

  1. It will not prove something for you without your help;
  2. It’s not a mathematician.

So, in this course we will be learning about the Lean proof assistant in general, and how to formalise and verify mathematical proofs.

Learning outcomes

  • Using Lean to prove mathematical results

Tentative schedule

Week Content
1 Introduction & Lean basics
2 Logic 1
3 Logic 2
4 Sets, the differences between sets and types, and a brief on what a type actually is
5 Projects introduction & Inductive types
6 Structures & type classes
7 Diamonds and deadline for choosing projects
8 Translating pen-and-paper mathematics to Lean 1
9 Translating pen-and-paper mathematics to Lean 2
10 Tactic writing, notation, etc…