Seminario Rubio de Francia: "Formalización de matemáticas en demostradores interactivos de teoremas" .- Jueves 30 de marzo
El jueves 30 de marzo de 2023 a las 12:00 h tendrá lugar una nueva conferencia de este ciclo, que impartirá José Divasón (Universidad de La Rioja). Se titula “Formalización de matemáticas en demostradores interactivos de teoremas”.
La charla tendrá lugar en el Aula 7 (primera planta, frente al Seminario Rubio de Francia) del Edificio B (Matemáticas) de la Facultad de Ciencias de la Universidad de Zaragoza.
NOTA: Esta es la charla que se tuvo que aplazar el 2 de marzo.
Resumen
Los demostradores interactivos de teoremas nos ayudan a probar formalmente resultados matemáticos con un ordenador. En los últimos años están teniendo un crecimiento importante, pero son todavía unos grandes desconocidos para la gran mayoría de matemáticos. En esta charla presentaremos estos sistemas de un modo divulgativo para intentar acercarlos a la figura del "matemático puro", incidiendo en la historia (pasado, presente y futuro), los fundamentos matemáticos subyacentes (lógicas, teorías de tipos, etc), además de qué y cómo se puede demostrar con ellos.
Enlace al resumen de la conferencia: http://anamat.unizar.es/seminario.html
