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.