This is the webpage for the course Preuve assistée par ordinateur dans Lean for the graduate school ED InfoMath, held in Lyon in February−March 2025.
The teacher is me/Filippo A. E. Nuccio: I am Maître de Conférences at the Université Jean Monnet Saint-Étienne and a member of the Institut Camille Jordan.
Classes will typically be in English, but any question in French (or in Italian…) is welcome; chances are high that the answer, if within my competences, will be in the same language. Feel free to reach out to me for any question, either by e-mail or o Zulip (see below for more on this).
In each lecture we will work on one file, whose solutions will be sent over by Zulip: the link below sends to a live version of the file that you can compile remotely without installing Lean, but this is a temporary solution and it is preferable to work on the project locally. For some lectures there is also a .pdf file with the discussed content.
Classes are on Wednesday, from 2PM to 5PM, at ENS-Lyon in the Salle de Conseil on the 3rd floor (except for the last one, that will take place on Thursday, April 3rd, from 1.30 PM to 4.30 PM). The preliminary schedule is as follows:
| Date | Topic | Accompanying file | Notes |
|---|---|---|---|
| Feb 19th | Introduction to proof assistants and to propositional calculus | Lean File Live Lean File |
We will also address installation and practical issues. |
| Feb 26th | Basic set theory and functions among sets | Lean File Live Lean File |
|
| Mar 12th | Formalizing algebraic structures | Lean File Live Lean File |
|
| Feb 19th | Formalizing topological spaces | Lean File Live Lean File |
|
| Apr 3rd | Formalizing analysis and more advanced topics | Subject to change according to participants’ taste and request. The class runs from 1.30 PM to 4.30PM |
You are required to perform the following tasks before the beginning of the course.
git installation, if you do not have
one yet: for some help, you can have a look at this page maintained by Patrick Massot.