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 `library_search`, `simp`, tactics
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	Overview of Type Theory
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

Cloning instructions

To clone this entire GitHub repository and install mathlib as a dependency, use
leanproject get https://github.com/adomani/Atelier_Lean_2023.git
This creates in the current directory a new directory called Atelier_Lean_2023, containing this repository and also a copy of mathlib.

Of course, the previous command assumes that you already have leanproject successfully installed on your computer.