This is the webpage for the Lean courses of the program “Higher Algebra and Formalised Mathematics” of the Advanced Master in Mathematics in Lyon for 2024/25. For the original git repository, click here.
Prerequisites
You will need to do the following tasks before the start of the course. We will help you do these tasks during the “Installation party” on September 4th.
- Make sure that you have a working wifi, usually via Eduroam.
- Install a working
gitinstallation: for some help, you can have a look at this page maintained by Patrick Massot. - Install a Lean editor (we strongly suggest that you install VSCode).
- Clone the course repository on your laptop using the address: https://github.com/faenuccio-teaching/M2Lyon2425.git (more about that during the “Installation Party”).
- Download the Mathlib build cache on your computer (more about that during the “Installation Party”).
- Create a GitHub account to be able later on to submit your work.
- Create an account to the Lean Community Chat on Zulip. Note you can use your GitHub account for that. Once you’ve got it, ask to one of the teachers to be invited to join the dedicated stream for this course.
- Administrative information about the program (dates, credits, internship, etc.) can be found here.
Teachers and schedule:
The three teachers for this course are Sophie Morel, Filippo A. E. Nuccio and Xavier F. Roblot. Feel free to contact us by e-mail or on Zulip (see the relevant point above).
First Term
Classes are on Wednesday, from 10AM to 1PM, at ENS-Lyon in room M7411 on the 4th floor. The schedule for the first term is as follows:
| Date | Topic | Teacher | Optional Link |
|---|---|---|---|
| Sep 4th | Installation Party | X. Roblot & S. Morel | |
| Sep 11th | Logic 1 | X. Roblot | |
| Sep 18th | Logic 2 | X. Roblot | |
| Sep 25th | Sets | F. Nuccio | Accompanying pdf file |
| Oct 2nd | Functions on Sets and Inductive Types | F. Nuccio | Accompanying pdf file |
| Oct 9th | Groups 1 | S. Morel | |
| Oct 16th | Groups 2 | S. Morel | |
| Oct 23rd | Rings and Fields 1 | X. Roblot | |
| Oct 30th | Holidays | — | |
| Nov 6th | Rings and Fields 2 | X. Roblot | |
| Nov 13th | Topological Spaces 1 | S. Morel | |
| Nov 17th | Deadline for project proposal | — | Upload it to your git branch |
| Nov 20th | Topological Spaces 2 | S. Morel | |
| Nov 27th | Calculus 1 | X. Roblot | |
| Dec 4th | Calculus 2 | X. Roblot |
Second Term
Classes are on Wednesday, from 9.45AM to 12.45PM, at ENS-Lyon, in room M7-411. The schedule for the second term is as follows:
| Date | Topic | Teacher | Notes |
|---|---|---|---|
| Jan 5th | Deadline for project submissions | — | |
| Jan 8th | Structures | X. Roblot | The class will finish at 12PM |
| Jan 15th | Inductive Types | F. Nuccio | Accompanying pdf file |
| Jan 15th | Projects presentations | Starting 1PM | |
| Jan 22nd | Classes and Instances 1 | F. Nuccio | |
| Jan 29th | Classes and Instances 2 | F. Nuccio | |
| Feb 5th | Categories in Lean 1 | S. Morel | |
| Feb 12th | Categories in Lean 2 | S. Morel | |
| Feb 19th | Introduction to Metaprogramming 1 | F. Nuccio | |
| Feb 26th | Categories in Lean 3 | S. Morel | |
| Mar 5th | Holidays | — | |
| Mar 12th | Introduction to Metaprogramming 2 | F. Nuccio |