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.

• Session 1:  26 Oct- Auditorio, Piso -1 .  

• Session 2:  27 Oct- Auditorio, Piso -1. 

• Session 3:  2 Nov- Sala 210 de Computación, Piso 2.