La matemática detrás de Lean, explicada para matemáticos
Una guía interactiva, de cero a experto, sobre cómo un asistente de pruebas convierte una demostración en un objeto que una máquina puede comprobar — y por qué eso funciona. Adaptada de una tesis de licenciatura en matemática que formalizó el teorema de completitud y la corrección de quicksort en Lean 4, sin una sola laguna.
¿Nuevo en Lean? El Preámbulo te enseña el lenguaje escribiendo expresiones desde cero, con la matemática al lado, antes de cualquier teoría. Si prefieres empezar por la motivación, ve al nivel 0.
El contrato con el lector
- Se asume madurez matemática: sabes leer definiciones, teoremas y demostraciones.
- No se asume nada de Lean, de teoría de tipos ni de ciencias de la computación.
- No tendrás que adivinar: cada paso lleva su justificación, cada resultado su demostración (o una referencia explícita), como en la tesis de la que nace esta guía.
La ruta
- PREÁMBULO Lean desde cero
- NIVEL 0 ¿Por qué verificar?
- NIVEL 1 El cálculo lambda
- NIVEL 2 Tipos simples (λ→)
- NIVEL 3 Lógica y deducción natural
- NIVEL 4 Curry–Howard
- NIVEL 5 El cubo-λ
- NIVEL 6 El CIC y Lean
- NIVEL 7 Completitud en Lean (experto)
- NIVEL 8 Quicksort verificado (experto)