El objetivo del libro Matemáticas en Lean es presentar el uso de Lean en el desarrollo formalizado de las Matemáticas. La presentación de hace mediante ejemplos y está basada en el libro Mathematics in Lean de Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis y Patrick Massot.
Los códigos del libro se encuentran en el repositorio Matematicas_en_Lean de GitHub.
El proyecto ForMatUS tiene como objetivo la formalización de las matemáticas enseñadas en la Universidad de Sevilla, fundamentalmente las asignaturas del Grado en Matemáticas.
Los sistemas elegidos, inicialmente, para la formalización son Isabelle/HOL y Lean.
El primero, Isabelle/HOL, se ha usado en la asignatura de Lógica matemática y fundamentos (de 3º del Grado en Matemáticas) y en la de Razonamiento automático (del Máster Universitario en Lógica, Computación e Inteligencia Artificial). Además, este curso los vídeos de las clases con Isabelle/HOL se han subido a YouTube en la lista Razonamiento con Isabelle/HOL que puede servir como introducción al uso del sistema.
El segundo, Lean, no se ha usado aún en ninguna de las asignaturas de la Universidad de Sevilla; pero sí he elaborado durante este curso algunos apuntes sobre el mismo:
El desarrollo del proyecto lo iré anunciando en Twitter con la etiqueta #ForMatUS.
Esta entrada es una recopilación de lecturas compartidas, durante julio de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante julio de 2020”
Esta entrada es una recopilación de lecturas compartidas, durante junio de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante junio de 2020”
Esta entrada es una recopilación de lecturas compartidas, durante mayo de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante mayo de 2020”