Eréndira Munguía Villanueva

¿Cómo puede la computadora ayudarte a corroborar la validez de algún resultado matemático? Los asistentes de demostraciones interactivos (interactive theorem provers) están diseñados justamente para este propósito, y están abriendo brecha en la investigación y la educación matemática. Charlaremos sobre algunos de los resultados más sonados obtenidos recientemente por la comunidad matemática al combinar estas herramientas con modelos de aprendizaje de máquina como los LLM’s (Large Language Model). Nos centraremos en el lenguaje Lean, uno de los asistentes más usados, sus fundamentos, similitudes y diferencias con otros lenguajes en la intersección de lógica y programación. Mostraremos algunos recursos para aprender y practicar Lean de forma gratuita y lúdica.

Palabras clave: Asistente de demostraciones interactivo, Lógica, Computación.