Resources
The most important resource is the Lean Community website. Here is a selection of resources from there, but feel free to look for more.- The Natural Number Game (NNG) (most beginner friendly)
- Tutorials project (Lean files with exercises)
- Mathematics in Lean (book in progress)
- Video lectures and exercises from LFTCM 2020
- Tutorial playlist (installation, working with projects,…)
- The Lean Zulip Chat (use your real name, please)
Meetings
Starting September 29th 2021, we meet on Wednesdays 15h-16h at room C3B/111 (UAB). Interested participants are encouraged to play the NNG before the first meeting, but we won’t assume they have done it. To communicate we use our own Zuplip chat, you can join it by clicking on the following invitation link: https://topologyleanuab.zulipchat.com/join/7hwtazwopr2czmjmtzpfvjln/Talks
On April 28, 2021 we had an invited talk by Joachim Kock (UAB). The video is available below.References after the talk
Thomas Jan Mikhail is providing us with a very good list of references: 1) Joachim mentioned Rijke’s book on HoTT which you can find here:https://github.com/EgbertRijke/HoTT-Intro On the same website there are also lecture notes on the same subject. 2) Joachim also mentioned HoTT’s standard reference, the HoTT book:
https://homotopytypetheory.org/book/ The HoTT book offers much more motivation. However the main body of the book develops type theory in an informal setting. This is a conscious decision; the aim is to present an alternative to the informal set theory used in “everyday mathematics”. Rijke’s book introduces type theory formally right from the start but offers less motivation. The HoTT book also contains a formal treatment, but it’s deferred to the appendix. 3) For a quick overview of HoTT I the following two papers can be helpful: Macor J. – A brief Introduction to Type Theory and the Univalence Axiom
https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf Grayson D. – An Introduction to Univalent Foundations for Mathematics
https://faculty.math.illinois.edu/~dan/Papers/ium.pdf Here are some further references on Type Theory. 4) Lambek, Scott – Introduction to Higher Order Categorical Logic 5) Martin-Löf – An Intuitionistic Theory of Types:
http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf Martin Löf – Intuitionistic Type Theory (Lecture Notes)
https://www.csie.ntu.edu.tw/~b94087/ITT.pdf