Curso de Doctorado: Formalización de matemáticas en Lean
María Inés de Frutos (Universidad Autónoma de Madrid)
8 ene 2023 - 10:04 CET
El curso será impartido por la profesora María Inés de Frutos durante el mes de febrero de 2023 en las fechas que se detallan más adelante.
El curso versa sobre el asistente de demostración y lenguaje de programación LEAN, herramienta que va cobrando importancia progresivamente en las matemáticas actuales. Una muestra de ello puede leerse en este artículo de divulgación de Quanta Magazine.
Se trata de un tema muy transversal que creemos puede interesar a un número elevado de estudiantes de diferentes áreas así como de profesores de la facultad.
Resumen del curso:
La formalización matemática soportada por un asistente de demostración consiste en digitalizar definiciones, resultados y demostraciones matemáticas. El objetivo de este curso es proporcionar una introducción a la formalización de matemáticas en el asistente de demostración de teoremas Lean 3. Para aprender a trabajar con Lean y su librería de matemáticas “mathlib”, formalizaremos ejemplos tomados de diversas áreas de las matemáticas, incluyendo lógica, álgebra, cálculo y topología.
El curso no asumirá experiencia previa en formalización. Las instrucciones para instalar Lean 3 y mathlib (antes de la primera sesión) están disponibles en el apartado “Regular Install” del enlace
https://leanprover-community.
Los ejercicios de cada sesión se podrán encontrar en el repositorio:
https://github.com/
Sobre la ponente: María Inés de Frutos trabaja actualmente en el Imperial College en Londres, en uno de los grupos donde el desarrollo de LEAN está siendo más importante, y próximamente se incorporará a la Universidad Autónoma de Madrid con un contrato Margarita Salas.
Duración: 12 horas
Cronología: La primera sesión introductoria tendrá lugar el lunes 6 de febrero de 9 a 11 en el Aula B12.
El resto de sesiones serán los días 8, 20, 22, 27 de febrero y 1 de marzo de 16 a 18 horas en el Aula B-07.
Inscripción: Por razones organizativas os animamos a inscribiros en este formulario, en particular es imprescindible si se quiere solicitar un certificado de participación. El curso está abierto a alumnos y profesores de otras universidades o centros a los que también les animamos a inscribirse en el formulario anterior.
El curso se podrá seguir online para aquellos participantes inscritos que así lo hayan solicitado.
Las grabaciones de las sesiones del curso se colgarán en el siguiente enlace.
Responsable del curso: María Pe Pereira