Atelier Lean 2023
Day 1, Tuesday May 2nd, 2023
Time | Speaker | Title |
---|---|---|
9.30-10.15 | Riccardo | What does it mean to formalise and why do it |
10.20-11.05 | Filippo | Formalising Math 1 |
11.05-11.35 | Coffee Break |
|
11.35-12.20 | Damiano | Generalizations, automation
|
12.25-13.10 | Filippo | Formalising Math 2 |
Lunch | ||
15-?? | Hacking session |
Day 2, Wednesday May 3rd, 2023
Time | Speaker | Title |
---|---|---|
9.30-10.15 | Damiano | |
10.20 -11.05 | Filippo | Formalising some basic Number Theory 1 |
11.05 -11.35 | Coffee Break |
|
11.35-12.20 | Riccardo | Lean Type Theory |
12.25 -13.10 | Filippo | Formalising some basic Number Theory 2 |
Lunch | ||
15-?? | Hacking session |
Formalisation Talks
Three talks (Tue 10.30-11.15 and 12.30-13.15; Wed 10.30-12.00) are devoted to getting our hands dirty trying to formalise some mathematics. During the afternoon hacking sessions, participants will try to solve exercices that are similar to the ones seen in class. The files used both in the lectures and for the hacking sessions can be tested online without installing Lean locally.
For each exercise session, click on the corresponding link below. You might have to wait for a minute or so until "Lean is busy..." becomes "Lean is ready!". Then, you can type exactly as I did in class. The only difference is that, instead of the nice "goals accomplished 🎉" you will see a more modest "no goals".
Part A: Logic. The Class and the Tutorial
Part B: Functions. The Class and the Tutorial
- Some Exercises on limits of real valued-functions.
Part C: Rings and Ideals. The Class and the Tutorial
Part D: some Number Theory
Links
- The Natural Number Game
- Lean community webpage
- Lean Zulip chat
- Damiano's slides on computers and maths
- Atelier PARI/GP, 2019
Cloning instructions
To clone this entire GitHub repository and install
mathlib
as a dependency, useleanproject get https://github.com/adomani/Atelier_Lean_2023.gitThis creates in the current directory a new directory called
Atelier_Lean_2023
, containing this repository and also a copy ofmathlib
.Of course, the previous command assumes that you already have
leanproject
successfully installed on your computer.