An introduction to Proof Assistants

Local organizers.  Daniel Barrera (USACh), Héctor del Castillo (USACh)

Speaker.  Riccardo Brasca (Université Paris-Cite)

Abstract. The goal of this mini-course is to give an introduction to formalization of mathematics. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.

Where. Departamento de Matemáticas y Ciencia de la Computación (USACH) and on ZOOM.