Para el curso utilizaremos archivos .lean, con el código disponible para ejecutarse o visualizarse en el Panel de Información (conocido como Infoview) que incluyen los editores de código con su respectivo modo para código de Lean. Además, se incluyen comentarios explicando el comportamiento y el contenido importante.
El material que se utilice lo podrás encontrar en el repositorio del curso. Se recomienda hacer un fork y procurar tener tus cambios en una rama distinta a la principal, para no tener conflictos en las actualizaciones.
Se utilizará durante el curso la versión de Lean número 4. Debido a que esta versión es relativamente reciente, y que la versión 3 tuvo mucho alcance, es posible encontrar material en internet que no compila en la versión más actual. Al revisar fuentes, procura revisar que se esté utilizando Lean 4.
Es importante que tengas tu propia instalación de Lean, para ello puedes remitirte a la guía oficial de instalación. También es recomendable revisar alguno de los siguientes enlaces según tu editor preferido:
Visual Studio Code: El editor "oficial" para código de Lean. Esta es la instalación sugerida, y es la que usaré durante el curso para asemejar lo más cercano a su experiencia.
Neovim: Plugin con soporte constante y en general buena interacción. Personalmente suelo utilizar esta opción.
Emacs: Modo para Lean 4, no cuenta con evil mode. Lo utilicé brevemente y es un buen paquete, no estoy al tanto de su mantenimiento en tiempos recientes.
Además, existen otras alternativas para ejecutar Lean.
URL: https://live.lean-lang.org/
Versión en línea del editor, que incluye el paquete de Mathlib (biblioteca popular con la formalización de una amplia diversidad de áreas de las matemáticas).
No es recomendable para el curso, puesto que utilizaremos nuestra propia biblioteca estándar. Puede ser útil para experimentos pequeños.
URL: https://github.com/jpyamamoto/syv-20252
Adicional al material del curso, el repositorio está configurado para poder ejecutar su propia instancia de VScode en el navegador. Esto te permitirá correr todo el ambiente que esperarías tener en tu instalación local, pero disponible a través del navegador.
La opción más recomendada es la instalación local, pero esta es una buena alternativa. Cuida subir tus cambios a tu repositorio, para no perder los avances.
A lo largo del curso utilizaré material adaptado del curso Hitchhiker's Guide to Logical Verification (2024 Edition) impartido por Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, y Jannis Limperg. Este material es desarrollado como parte del proyecto Lean Forward.
Además de los archivos de Lean que usaremos, puedes revisar el libro de texto "The Hitchhiker's Guide to Logical Verification".
Functional Programming in Lean: Un libro digital que introduce Lean desde el enfoque de la programación funcional.
Theorem Proving in Lean: Un libro digital que introduce a Lean utilizando el enfoque de la realización de demostraciones matemáticas.
Formalising Mathematics: Acompañamiento de un curso en donde se enseña Lean aplicado a distintas áreas matemáticas como la teoría de conjuntos, grupos, espacios topológicos, teoría de números, y más.
The Natural Number Game: Un curso interactivo en línea donde se construye cierta teoría sobre los números naturales y se demuestran teoremas varios sobre operaciones aritméticas.