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
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.
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.
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.