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:

  • 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.