Pasen y Lean

Start: 2 October 2024 09:00
End: 2 October 2024 10:00
Categories: Conference , Seminar , Instituto de Matemáticas UGR

Where: Seminario Departamento Análisis Matemático, Facultad de Ciencias

IMAG Functional Analysis Seminar
Title: "Pasen y Lean"
By Esteban Martínez Vañó (Universidad de Granada)
Abstract: En este pequeño seminario hablaremos sobre qué son los interactive theorem provers, por qué usarlos y cómo podemos hacerlo. Con más detalle, un interactive theorem prover es un programa que asiste al usuario en la formalización (dentro de un marco lógico puramente sintáctico) de resultados matemáticos de modo que un ordenador puede vericar su validez. A lo largo de la charla veremos pues algunos resultados famosos formalizados en este tipo de programas, el interés que puede tener hacerlo, un (muy) breve vistazo a la lógica subyacente y algunos ejemplos prácticos sobre cómo usar uno de ellos conocido como Lean.