Formalizing mathematical proofs in a way that can be checked by a
computer is an idea as old as computer science, and has been an active
field of research for many years. Recently, a very active community of
mathematicians and computer scientists has formed around the
interactive theorem prover Lean, making formalization more accessible
and usable to non experts. The goal of this seminar is to learn the
basics of Lean and to explore some of the amazing formalization
projects of the last few years, in particular the library mathlib.
- verantwortliche Lehrperson: Simon Pepin-Lehalleur
ePortfolio: Nein