La ruta de aprendizaje
Un preámbulo práctico y nueve módulos teóricos, en orden de dependencia. La numeración de definiciones y teoremas coincide con la de la tesis, de modo que siempre puedes contrastar la guía con el documento original.
Preámbulo Lean desde cero
El lenguaje en la práctica: expresiones, tipos, funciones y pruebas construidas una a una, hasta leer un teorema real de la tesis.
Nivel 0 ¿Por qué verificar?
El problema de confiar en las demostraciones, la historia de la formalización y qué promete un asistente de pruebas.
Nivel 1 El cálculo lambda
El lenguaje universal de las funciones: términos, sustitución, α-conversión, β-reducción, formas normales y confluencia.
Nivel 2 Tipos simples (λ→)
El cálculo lambda simplemente tipado: juicios, reglas de tipado, Church y Curry, decidibilidad.
Nivel 3 Lógica y deducción natural
Demostrabilidad (⊢) y verdad (⊨): deducción natural, tablas de verdad, solidez y la completitud de Kalmár.
Nivel 4 Curry–Howard
Proposiciones como tipos, pruebas como términos: el puente exacto entre la lógica y el cálculo lambda.
Nivel 5 El cubo-λ
Tres formas de dependencia (λ2, λω̲, λP) y su combinación en el Cálculo de Construcciones.
Nivel 6 El CIC y Lean
Tipos inductivos, recursores y eliminadores: el cálculo que Lean implementa, y las tácticas como constructores de términos.
Nivel 7 Completitud en Lean (experto)
La formalización completa del teorema de completitud: cada definición y cada lema, en matemática y en Lean, lado a lado.
Nivel 8 Quicksort verificado (experto)
La corrección de un algoritmo con el mismo método: especificación, terminación, permutación y ordenamiento.