Javier Villar Ortega (Universidad de La Rioja) impartirá la conferencia "Mecanización de pruebas: métodos topológicos y algebraicos para el desarrollo automático de demostraciones"

El trabajo de Per Martin-Löf en el desarrollo de lenguajes de programación funcionales que pudiesen expresar la sintaxis de las Matemáticas, produjo un amplio panorama de posibilidades para la creación de herramientas computacionales de asistencia para la demostración. Esto es, software diseñado para permitir traducir argumentos matemáticos a sentencias de un lenguaje de programación, a través de una correspondencia de tipo Curry-Howard, que permita usar los informes generados por sus compiladores como evidencia de la veracidad de demostraciones.
Esta clase de herramientas se están convirtiendo recientemente en particularmente atractivas por dos desarrollos recientes: una gran popularización de algunas de ellas, como el lenguaje Lean, que están apoyando la creación de grandes librerías de Matemáticas verificadas formalmente; y el enfoque reciente del empleo de LLMs para la creación automática de texto matemático, que está presionando los mecanismos de revisión a pares por el enorme volumen de propuestas, y forzando a buscar nuevas vías para construir confianza frente a textos cuya redacción posiblemente no ha involucrado a un ser humano.
En esta charla, hablaremos de un ejemplo paradigmático de teoría de tipos: la familia de las teorías univalentes, recogidas en el estudio de la Teoría Homotópica de Tipos. De reciente creación, este campo ha ganado una gran atención por su capacidad de combinar tecnología matemática de múltiples áreas, como puede ser la Topología Algebraica, la Lógica de Orden Superior y la Teoría de Categorías (Superiores). Un estudio en detalle de este área nos permitirá explorar las ventajas y límites de las herramientas de asistencia de demostración, la clase de axiomáticas alternativas que pueden exigir, y su relación con la Matemática Clásica.