Proyecto ForMatUS (Formalización de las Matemáticas de la US)
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:
- Lógica y demostración con Lean es un resumen del curso Logic and proof (de Jeremy Avigad, Robert Y. Lewis y Floris van Doorn).
- Deducción natural en Lean es una presentación de las reglas de deducción natural en Lean mediante ejemplos básicos.
- Tácticas básicas de Lean es un resumen de las tácticas básicas de Lean, con ejemplos, basado en Basic guide to tactics de Kevin Buzzard.
- Demostraciones aplicativas en Lean es una adaptación del capítulo 5 (Tactics) del libro Theorem proving in Lean de Jeremy Avigad, Leonardo de Moura y Soonho Kong.
- Interacción con Lean es una adaptación del capítulo 6 (Interacting with Lean) del libro Theorem proving in Lean de Jeremy Avigad, Leonardo de Moura y Soonho Kong.
- Tipos inductivos en Lean es una adaptación del capítulo 7 (Inductive types) del libro Theorem proving in Lean de Jeremy Avigad, Leonardo de Moura y Soonho Kong.
- Inducción y recursión en Lean es una adaptación del capítulo 8 (Induction and recursion) del libro Theorem proving in Lean de Jeremy Avigad, Leonardo de Moura y Soonho Kong.
- Resúmenes de Lean es una recopilación de enlaces con resúmenes sobre sintaxis y tácticas de Lean
El desarrollo del proyecto lo iré anunciando en Twitter con la etiqueta #ForMatUS.