Welcome

This website contains the basic information about the Graduate Course Preuve assistée par ordinateur dans Lean for the École Doctorale Info-Math de Lyon, in Spring 2026.

The teacher is Filippo A. E. Nuccio and all material is in English: classes will be in French or in English according to participants.

For every lecture, there is a .md file (exported also as a .pdf), that you find below and that contains all material discussed in class; alongside these files, there is also a .lean file shown during class, whose solutions are posted the day following the lecture, in general.

The Mathlib commit upon which this project is build is 32d2424: the documentation for the Mathlib version used in this project is available here.

Agenda

Classes take place from 13h30 to 16h30 (with one exception on March 18th) at the “site Monod” of the École Normale Supérieure, in room 316C on the third floor (accessible from the coffee corner).

Date	Lecture	Ancillary Files	Notes
Fri, March 13th	Tactics and Types	Files Lean, MarkDown and PDF.
Wed, March 18th	More on Types	Files Lean, MarkDown et PDF	Warning The course is 14h00–17h00
Fri, March 20th	Algebra 1	Files Lean, MarkDown and PDF
Wed, April 1st	Algebra 2	same files as for the previous lecture
Fri, April 3rd	Sets

References

There aren’t many books detailing how Lean works, but the beautiful

• Mathematical Components, by A. Mahboubi and E. Tassi,

tailored around the proof assistant Rocq, is an excellent introduction to what the formalisation of mathematics is. The third chapter contains a nice introduction to the “type theory” that we use.

Another survey of what is needed type-theoretically can be found in the first chapter “Type theory” of the

• Homotopy Type Theory (a.k.a. “HoTT book”)

A more complete source, extremely well written and a really pleasant read is

• Lectures on the Curry–Howard Isomorphism, by M. H. Sørensen et P. Urzyczyn.

The two Lean-oriented references

• Theorem Proving in Lean 4, by J. Avigad, L. de Moura, S. Kong et S. Ullrich
• Mathematics in Lean, by J. Avigad et P. Massot

also contain a lot of material relevant to our course.

Lean and GitHub prerequisites

Before the beginning of the course (on Friday, March 13th 2026), make sure to:

• have a working internet connection once at ENS, ideally through Eduroam;
• have a working git installation: in case you need help, you can try to have a look at the nice tutorial maintained by Patrick Massot;
• have a an account on GitHub to be able to upload your work;
• have a working installation of Lean on your laptop, by following the offical instructions. Shall you run into problems, don’t panic: we’ll discuss everything during the first lecture;
• have downloaded (through git clone) the repository of this course, available at https://github.com/faenuccio-teaching/GradCourse26.git;
• have disabled all Chat AI Features from VSCode: for this, go to Settings → Features → Chat and select Disable AI Features.