Skip to content

This is the repository for the Lean master program in Lyon for 2024-25

Notifications You must be signed in to change notification settings

faenuccio-teaching/M2Lyon2425

Repository files navigation

M2Lyon2425

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 git installation: 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 15th 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 10AM to 1PM, at ENS-Lyon. The schedule for the second term is as follows:

Date Topic Teacher Optional Link
Jan 8th Structures X. Roblot
Jan 15th Inductive Types F. Nuccio
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

Exams

About

This is the repository for the Lean master program in Lyon for 2024-25

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •  

Languages