En el vídeo se comentan distintas pruebas con Lean de una igualdad con productos de números reales. La primera es por reescritura usando las propiedades asociativa y conmutativa, La segunda es con encadenamiento de ecuaciones. Las restantes son automáticas.
Los enlaces correspondientes son a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan distintas pruebas con Lean de la transitividad de la igualdad de los números reales y cómo se trabaja con ellas en Lean Web. Las primeras son mediante reescritura y las últimas son automáticas.
Los enlaces correspondientes son a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
Dentro del proyecto ForMatUS el primer subproyecto, titulado “DAO (Demostración Asistida por Ordenador) con Lean” tiene como base la lógica que se estudia en las asignaturas de
El objetivo concreto de este subproyecto es presentar una introducción a la DAO (Demostración Asistida con Ordenador) usando Lean para usarla en las clases de la asignatura de Razonamiento automático. Por tanto, el único prerrequisito es, como en el Máster, cierta madurez matemática como la que deben tener los alumnos de los Grados de Matemática y de Informática.
La exposición se hará mediante una colección de ejercicios. En cada ejercicios se mostrarán distintas pruebas del mismo resultado y se comentarán las tácticas conforme se van usando y los lemas utilizados en las demostraciones.
Además, para cada ejercicio se proporcionan tres enlaces:
El proyecto se desarrollará en
En el siguiente vídeo se presenta el proyecto:
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.