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.