Formalizing mathematics in LEAN

As mathematical research advances, researchers become more and more specialized, and the mathematics they produce becomes more and more complicated to verify.
The possibility to formalize and check proofs thanks to computer programs is thus more relevant than ever. What’s more, tremendous progress in recent years make it so that formalizing actual research level mathematics is possible, and formalizing student level mathematics is accessible to students.

In this seminar, students will practice with the LEAN proof assistant. We meet weekly on Zoom, and discuss informally: each student gets a chance to speak, to explain the work they have done in previous weeks, and to plan ahead.
Students may obtain up to 8 credit points, by formalizing a theorem or new definitions, thus contributing to mathlib, the library which gathers all mathematics that has already been formalized in LEAN.
Topics suitable to both MSc and BSc students will be offered, no prior knowledge is required.