Aprender Lean 4 — guía y recursos (v2, con vídeos)

Conversación: Lean 4 tutorial · rel. Lean dependent type theory. Índice: documentos.

Para formalización de matemáticas.

1. Ruta de aprendizaje recomendada

• Natural Number Game: el punto de partida ideal. Un juego interactivo en el navegador donde demuestras teoremas sobre números naturales desde cero. No requiere instalar nada. https://adam.math.hhu.de/#/g/leanprover-community/nng4
• Mathematics in Lean: el siguiente paso. Orientado a matemáticas de verdad. El capítulo 5 cubre teoría elemental de números. https://leanprover-community.github.io/mathematics_in_lean/
• Theorem Proving in Lean 4 (TPiL): el manual de referencia. Más sistemático, cubre los fundamentos a fondo. https://leanprover.github.io/theorem_proving_in_lean4/
• Página de aprendizaje de la comunidad (índice de todos los recursos): https://leanprover-community.github.io/learn.html

2. Qué es Lean y hasta dónde llega

Lean 4 es un asistente de demostración y lenguaje de programación. Para matemáticas, su mayor activo es Mathlib, una biblioteca colaborativa de más de un millón de líneas con matemática formalizada.

Hasta dónde llega hoy:

• 85 de los «100 teoremas» clásicos están formalizados en Lean. https://leanprover-community.github.io/100.html
• Proyectos de frontera: el teorema de Freiman-Ruzsa polinómico (liderado por Terence Tao), el Liquid Tensor Experiment (Scholze) y el Último Teorema de Fermat (en curso).
• Artículo reciente de Terence Tao sobre fiabilidad de Lean y la IA (9 oct. 2026): https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/

3. Teoremas clásicos ya formalizados (ejemplos)

• Infinitud de los números primos
• Irracionalidad de la raíz de 2
• Teorema fundamental del álgebra
• Ley de reciprocidad cuadrática
• Teorema de los cuatro colores
• Teorema fundamental del cálculo

4. Tutoriales hechos por particulares

• Architecture & Performance, «My first Lean 4 proof: the irrationality of sqrt 2» (paso a paso, muy didáctico): https://architecture-performance.fr/en/blog/my-first-lean-4-proof-the-irrationality-of-sqrt2
• Repositorio absolukie/lean-practice (ejercicios resueltos): https://github.com/absolukie/lean-practice
• Brandon Rozek, tutorial de Lean 4: https://brandonrozek.com/blog/lean4-tutorial/
• Lambdaclass, «The Hitchhiker’s Guide to Reading Lean 4 Theorems»: https://blog.lambdaclass.com/the-hitchhikers-guide-to-reading-lean-4-theorems/
• emallson, «A Beginner’s Companion to Theorem Proving in Lean»: https://emallson.net/blog/a-beginners-companion-to-theorem-proving-in-lean/

5. Herramientas útiles

• Loogle: buscador de lemas de Mathlib por tipo o nombre. https://loogle.lean-lang.org
• VS Code con la extensión de Lean 4 y el panel InfoView (muestra el estado de la demostración en tiempo real).
• elan (gestor de versiones), lake (gestor de proyectos) y mathlib4 (la biblioteca).

6. Fundamentos teóricos: el cálculo de construcciones inductivas

Lean 4 está basado en el Cálculo de Construcciones Inductivas (CIC), una teoría de tipos dependientes. La implicación es una función (de p a q), y proposiciones y demostraciones se identifican vía la correspondencia de Curry-Howard (proposiciones como tipos). El tipo Prop es Sort 0, la base de la jerarquía de universos.

• Theorem Proving in Lean 4, caps. 2 y 3: https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory/ y https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/
• A Tour of Type Theory (Univ. de Colorado): https://math.colorado.edu/~chme3268/assets/documents/type-theory.pdf
• Computer-assisted proofs in Lean 4 (Bachelor’s Project, 2025): https://fse.studenttheses.ub.rug.nl/37126/1/bMATH2025NijholtJ.pdf
• Lean and its type theory (curso de Pfaffelhuber): https://pfaffelh.github.io/leancourse/Lean-and-its-type-theory/
• Vídeo: «What are dependent types, aka the Calculus of Construction»: https://www.youtube.com/watch?v=cf3hVL1bgNc

7. Tutoriales en vídeo

Curso «Lean for the Curious Mathematician» (ICERM, 2022) — clases grabadas de los principales expertos de la comunidad, pensadas para matemáticos:

• Jeremy Avigad, introducción a Lean: https://mathinstitutes.org/videos/19287
• Kevin Buzzard, Natural Number Game, demo y ejercicios (encaja con el primer paso de la ruta): https://mathinstitutes.org/videos/19288
• Jeremy Avigad, lógica: https://mathinstitutes.org/videos/19290
• Robert Lewis, estructuras y clases: https://mathinstitutes.org/videos/19293
• Patrick Massot, cálculo: https://mathinstitutes.org/videos/19297
• Leonardo de Moura (creador de Lean), Lean 4: https://mathinstitutes.org/videos/19300

Kevin Buzzard, curso «Formalising Mathematics» (Imperial College): lista de YouTube donde resuelve las hojas de problemas y explica técnicas. Ojo: usa Lean 3, la sintaxis difiere algo, pero las ideas y tácticas se trasladan bien. El enlace a la lista está en la página del curso: https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/

Glimpse of Lean (Patrick Massot): introducción práctica de 2-3 horas, usada en cursos universitarios como paso previo a Mathematics in Lean: https://www.andrej.com/zapiski/MAT-FORMATH-2024/book/04-first-encounter-with-lean.html