Seminar on Lean
Please register here.
Time: Fridays, 13:00 - 15:00
Place: Y27H12 in Campus Irchel (Institut für Mathematik, UZH)
Prerequisites: Essentially none. We expect a very diverse audience, so there will be no specific mathematical prerequisites. There are also no programming prerequisites! We aim to introduce Lean from scratch, and learn to use it together.
Organisers: Elif Saçıkara & Ödül Tetik
Objectives and syllabus
This informal seminar course aims to gather participants from different backgrounds to understand the basics of Lean, a computer proof assistant. We will also cover some relevant type theory. A putative syllabus can be found here.
Notes
Week 1 (ES) - slides
Week 2 (ÖT) - Logic, categories, types*
Week 3 (ES) - first draft of the notes
Week 4 (ÖT) - More types, AoC* - Screenshot of Lean code to prove type-theoretic AoC.
Week 6 (MF) - handout
*An extended typed version with references coming soon.
References & Useful Links
The mother of all Lean websites.
This is the Lean 3 handbook. We will not be using Lean 4, as the library has not yet been adapted.
Instructions to install Lean and mathlib, the mathematical library. Please make sure that you install Lean 3!
We will use some material from this standard reference in the theoretical component of this seminar.
We will steal some exercises from here.
Zulip chats: for the general community and for Zürich. Here you may post your questions and join the discussions.