Lean 4 para matemáticos: guía docente
Presentación
A quién va dirigida. Esta guía está dirigida a profesores que deseen presentar Lean 4 a estudiantes de Matemáticas acostumbrados a demostrar en papel pero sin experiencia previa en programación. No se requiere ningún conocimiento previo de informática.
Filosofía del curso.
- Lean es un cuaderno de demostraciones que contesta. Escribes un argumento y el ordenador te dice, paso a paso, qué te falta. Se presenta como un interlocutor paciente, no como un lenguaje de programación.
- Primero matemáticas, luego sintaxis. Cada tema parte de una demostración que el estudiante ya sabe hacer en papel y la traduce a Lean.
- Cero instalación al principio. Las tres primeras sesiones se pueden hacer en el navegador. La instalación local llega cuando el estudiante ya quiere seguir solo.
- Se aprende leyendo el estado de la prueba. La habilidad central no es memorizar tácticas, sino leer la ventana de objetivos (el infoview) como quien lee una pizarra.
- Equivocarse es barato. El error en rojo es información, no un fracaso.
Estructura. Ocho temas de unas 2 horas cada uno (teoría y práctica mezcladas). Cada tema tiene dos partes: el contenido (lo que ve el estudiante) y los consejos didácticos (notas para el profesor con ideas clave, errores típicos, ...).
Convención. Todos los ejemplos empiezan con import Mathlib.Tactic, la biblioteca de tácticas de Lean. Los bloques de código se pueden pegar tal cual en el editor.
| Tema | Título | Idea central |
|---|---|---|
| 1 | Primer contacto | Un teorema es un tipo; una demostración es un término |
| 2 | Lógica proposicional | Conectivas y las tácticas que los manejan |
| 3 | Cuantificadores y conjuntos | ∀, ∃, pertenencia, inclusión |
| 4 | Igualdad y cálculo |
rw, calc, ring, linarith
|
| 5 | Inducción y recursión | Naturales, sumatorios, definiciones recursivas |
| 6 | Definiciones propias |
def, structure, límites |
| 7 | Moverse por Mathlib | Buscar lemas sin saberlos de memoria |
| 8 | Proyecto final | Formalizar un resultado propio |