Orador: Riccardo Brasca (Université Paris-Cité)
Titulo: An introduction to proof assistants: a mini course about mathematical formalization
Fechas: tres sesiones:
26/10: 15h- 16h30
27/10: 15h- 16h30
02/11: 11h30- 13h
Lugar: en el DMCC (USACH) y online por el link https://reuna.zoom.us/j/8697753194?pwd=Uno1anhrMXQ1WHhpa0FFNTRJRTExdz09.
Resumen: 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.