APRENDER LEAN 4 - GUÍA Y RECURSOS
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/
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