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.

1. 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.
2. 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.
3. 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.
4. 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.
5. 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 la consejos didácticos (notas para el profesor: ideas clave, errores típicos, ...).

Convención. Todos los ejemplos empiezan con import Mathlib.Tactic, la biblioteca de tácticas matemática de Lean. Los bloques de código se pueden pegar tal cual en el editor.

Tema 1. Primer contacto

Contenido

Objetivos. Abrir Lean, escribir un enunciado, leer el estado de la prueba y cerrar una demostración muy sencilla.

1.1 Qué es Lean (en tres frases). Lean es un asistente de demostraciones: comprueba que cada paso de un argumento es lógicamente correcto. Los enunciados se escriben en un lenguaje muy cercano al matemático. Una demostración aceptada por Lean no admite lagunas.

1.2 Dónde escribir. Para empezar basta el editor web de Lean. A la izquierda se escribe; a la derecha aparece el infoview, que muestra lo que Lean responde. Para trabajar en local se usa Visual Studio Code con la extensión de Lean 4, que guía la instalación.

1.3 Tu primer enunciado

import Mathlib.Tactic

example : 2 + 2 = 4 :=
by norm_num

Lectura: «Ejemplo: 2 + 2 = 4. Demostración: calcula con norm_num.» La palabra example introduce un enunciado sin nombre; by anuncia que vamos a demostrar con tácticas, que son órdenes del tipo «aplica este resultado», «calcula», «separa en casos».

1.4 Hipótesis y objetivo. Coloca el cursor tras by en el ejemplo siguiente:

example
  (a b : ℕ)
  (h : a = b)
  : b = a :=
by
  exact h.symm

El infoview muestra:

a b : ℕ
h : a = b
⊢ b = a

Sobre la línea ⊢ están las hipótesis (lo que tenemos); tras ⊢ está el objetivo (lo que queremos). Toda la técnica de Lean consiste en transformar el objetivo hasta que se cierra. exact h.symm dice: «el objetivo se obtiene exactamente de h dándole la vuelta».

1.5 Teoremas con nombre.

theorem suma_comm
  (a b : ℕ)
  : a + b = b + a :=
by
  exact Nat.add_comm a b

theorem suma_comm'
  (a b : ℕ)
  : a + b = b + a :=
by
  ring

ℕ se escribe \N y el editor lo convierte solo; lo mismo \R para ℝ, \to para →, \forall para ∀, \ex para ∃. Dos demostraciones del mismo hecho: una citando un lema, otra calculando. Ambas son válidas.

1.6 La idea de fondo, sin dramatizar. En Lean los enunciados son tipos y las demostraciones son elementos de esos tipos. No hace falta entender la teoría de tipos para empezar: basta saber que h : a = b significa « h es una demostración de que a = b » y que se usa como cualquier otro dato.

Ejercicios.

1. Demuestra

    example
      (a b c : ℕ)
      (h1 : a = b)
      (h2 : b = c)
      : a = c

con `exact h1.trans h2`.

1. Demuestra

    example
      (x : ℝ)
      : x + 0 = x

con `ring`, y después con `exact add_zero x`.

1. Cambia el enunciado de suma_comm a algo falso (por ejemplo a + b = b + a + 1) y lee el error. ¿Qué te dice Lean que falta?
2. Pon sorry en lugar de una demostración. ¿Qué diferencia hay en el color y en el mensaje?

Consejos didácticos

• Idea que debe quedar clara. El infoview es la pizarra. Si el estudiante se pierde, la respuesta casi siempre es «mira el objetivo».
• Cómo presentarlo. Empieza con una demostración en papel de a = b → b = a y hazla en paralelo en Lean. El estudiante debe ver que el razonamiento es el mismo.
• Errores frecuentes.
  • Olvidar import Mathlib.Tactic.
  • Escribir ASCII (->) y no entender por qué cambia: ambos valen, pero conviene unificar.
  • Sangría: tras by, las líneas deben ir indentadas y alineadas.
  • Confundir = con :=.
• Sobre la teoría de tipos. Mantén el discurso al mínimo. Si preguntan, responde brevemente y emplaza al Tema 6.
• Truco para quitar miedo. Deja que rompan cosas a propósito. Un error de Lean casi nunca es grave, y verlo pronto vacuna.

Tema 2. Lógica proposicional

Contenido

Objetivos. Manejar →, ∧, ∨, ¬, ↔ con las tácticas básicas. Cada conectiva tiene una forma de construirlo y otra de usarlo.

2.1 Proposiciones. P Q : Prop declara dos proposiciones cualesquiera. Una hipótesis hP : P dice que P es verdadera.

2.2 Tabla de tácticas.

2.3 Ejemplos.

example
  (P Q : Prop)
  : P ∧ Q → Q ∧ P :=
by
  intro h
  -- h : P ∧ Q
  -- ⊢ Q ∧ P
  obtain ⟨hp, hq⟩ := h
  -- hp : P
  -- hq : Q
  exact ⟨hq, hp⟩

example
  (P Q : Prop)
  (hP : P)
  (hQ : Q)
  : P ∧ Q :=
by
  constructor
  · -- ⊢ P
    exact hP
  · -- ⊢ Q
    exact hQ

example
  (P Q : Prop)
  : P ∨ Q → Q ∨ P :=
by
  intro h
  -- h : P ∨ Q
  -- ⊢ Q ∨ P
  rcases h with hp | hq
  · -- hp : P
    right
    -- ⊢ P
    exact hp
  · -- hq : Q
    left
    -- ⊢ Q
    exact hq

example
  (P Q : Prop)
  (h : P → Q)
  (hnq : ¬ Q)
  : ¬ P :=
by
  intro hp
  -- hp : P
  -- ⊢ False
  exact hnq (h hp)

Detrás de cada paso he anotado, como un comentario que empieza con --, los cambios que origina dicho paso en las hipótesis o en el objetivo. Estos comentarios son opcionales y no forma parte de la demostración.

El punto · abre un subobjetivo: tras constructor hay dos metas y cada punto se ocupa de una.

2.4 Lectura matemática. El segundo ejemplo es «supongamos P y Q; entonces tenemos Q y P». intro es supongamos; obtain es descomponemos la hipótesis; exact es concluimos.

Ejercicios.

1. P ∧ (Q ∧ R) → (P ∧ Q) ∧ R.
2. (P → Q) → (Q → R) → (P → R).
3. P ∨ Q → (P → R) → (Q → R) → R.
4. ¬ (P ∧ ¬ P).
5. Reto: (P ↔ Q) → (Q ↔ P).

Consejos didácticos

• Estrategia. Presenta siempre la pareja construir / usar. Es el hilo conductor de todo el curso y reaparecerá con ∀ y ∃.
• Errores frecuentes.
  • Intentar exact cuando falta un intro.
  • No ver que ¬ P es P → False.
  • Olvidar el punto · o indentarlo mal; Lean avisa de «unsolved goals».
• Recurso útil. Enseña assumption (cierra el objetivo si coincide con una hipótesis) y tauto (resuelve tautologías) solo después de que hayan hecho los ejercicios a mano. Si no, tauto anula el aprendizaje.
• Lógica clásica. Mathlib es clásica: by_contra, by_cases y push_neg están disponibles. Menciónalo sin entrar en constructivismo, salvo que el grupo lo pida.

Tema 3. Cuantificadores y conjuntos

Contenido

Objetivos. Usar ∀ y ∃, y trabajar con conjuntos mediante pertenencia, inclusión e igualdad por doble inclusión.

3.1 Cuantificadores. Siguen el mismo patrón construir / usar.

example : ∃ n : ℕ, n * n = 16 :=
by
  use 4

example
  (f : ℝ → ℝ)
  (hf : ∀ x, f x = 2 * x + 1)
  : f 3 = 7 :=
by
  rw [hf]
  -- ⊢ 2 * 3 + 1 = 7
  norm_num

example
  (P : ℕ → Prop)
  (h : ∃ n, P n)
  : ¬ ∀ n, ¬ P n :=
by
  intro h1
  -- h1 : ∀ (n : ℕ), ¬P n
  -- ⊢ False
  obtain ⟨n, hn⟩ := h
  -- n : ℕ
  -- hn : P n
  exact h1 n hn

3.2 Conjuntos. Set ℕ es el tipo de subconjuntos de ℕ. x ∈ A ∩ B es, por definición, x ∈ A ∧ x ∈ B, así que las tácticas del Tema 2 funcionan directamente.

example
  (A B : Set ℕ)
  : A ∩ B ⊆ A :=
by
  intro x hx
  -- x : ℕ
  -- hx : x ∈ A ∩ B
  -- ⊢ x ∈ A
  exact hx.1

example
  (A B : Set ℕ)
  : A ∩ B = B ∩ A :=
by
  ext x
  -- ⊢ x ∈ A ∩ B ↔ x ∈ B ∩ A
  constructor
  · -- ⊢ x ∈ A ∩ B → x ∈ B ∩ A
    rintro ⟨hA, hB⟩
    -- hA : x ∈ A
    -- hB : x ∈ B
    -- ⊢ x ∈ B ∩ A
    exact ⟨hB, hA⟩
  · -- ⊢ x ∈ B ∩ A → x ∈ A ∩ B
    rintro ⟨hB, hA⟩
    -- hB : x ∈ B
    -- hA : x ∈ A
    -- ⊢ x ∈ A ∩ B
    exact ⟨hA, hB⟩

ext x es el principio de extensionalidad: «sea x un elemento; probemos que está en un lado si y solo si está en el otro». rintro es intro más obtain en un solo paso.

Ejercicios.

1. ∃ x : ℝ, x + 3 = 5.
2. (∀ x, P x ∧ Q x) → ∀ x, P x.
3. A ⊆ B → B ⊆ C → A ⊆ C para conjuntos de ℕ.
4. A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C). Es larga; hazla primero en papel.
5. Reto: (∃ x, ∀ y, R x y) → ∀ y, ∃ x, R x y.

Consejos didácticos

• Punto delicado. El orden de los cuantificadores. Pide que lean en voz alta el enunciado y el objetivo tras cada táctica.
• Error frecuente. Dar el testigo demasiado pronto o demasiado tarde: en ∀ ε, ∃ δ, … primero intro ε, luego use; si se invierte el orden, la demostración deja de ser posible. Es una excelente ocasión para que vean por qué el orden importa.
• Sobre Set. Muchos estudiantes esperan que x ∈ A ∩ B sea opaco. Muéstrales que es transparente: hx.1 funciona.
• Doble inclusión. Conviene enseñar Set.Subset.antisymm como alternativa a ext, pero solo como curiosidad.

Tema 4. Igualdad y cálculo

Contenido

Objetivos. Reescribir con rw, encadenar igualdades con calc y dejar que Lean haga el álgebra rutinaria.

4.1 Reescribir. rw [h] sustituye en el objetivo cada ocurrencia del lado izquierdo de h por el derecho.

example
  (a b c : ℕ)
  (h1 : a = b)
  (h2 : b = c)
  : a = c :=
by
  rw [h1]
  -- ⊢ b = c
  rw [h2]

example
  (a b c : ℕ)
  (h1 : a = b)
  (h2 : b = c)
  : a = c :=
by
  rw [h1, h2]

4.2 Cálculo en cadena. Lean permite escribir la demostración como lo haríamos en una pizarra:

example
  (a b : ℝ)
  (h : a = 2 * b)
  (hb : b = 3)
  : a = 6 :=
by
  calc a = 2 * b := h
       _ = 2 * 3 := by rw [hb]
       _ = 6     := by norm_num

Cada línea es una igualdad con su justificación. El guion bajo _ significa «lo de la línea anterior».

4.3 Demostraciones automáticas.

example
  (a b : ℝ)
  : (a + b)^2 = a^2 + 2*a*b + b^2 :=
by
  ring

example
  (a b : ℝ)
  (h : a ≤ b)
  : a + 1 ≤ b + 1 :=
by
  linarith

example
  (a b : ℝ)
  : a * b ≤ (a^2 + b^2) / 2 :=
by
  nlinarith [sq_nonneg (a - b)]

En el último ejemplo, sq_nonneg (a - b) es la pista: el hecho 0 ≤ (a - b)^2. Es exactamente lo que diríamos en papel.

Ejercicios.

1. (a + b) * (a - b) = a^2 - b^2 en ℝ con ring.
2. Demuestra el 4.2 con rw y norm_num sin calc.
3. a ≤ b → c ≤ d → a + c ≤ b + d con linarith.
4. 0 ≤ a^2 + b^2 con positivity.
5. Reto: 2*a*b ≤ a^2 + b^2 con nlinarith y la pista adecuada.

Consejos didácticos

• Equilibrio. Muchos estudiantes descubren ring y linarith y los usan para todo. Está bien: son demostradores de aritmética, no atajos tramposos. Lo que sí conviene es que sepan hacer la versión larga con calc cuando la automática falla.
• Cuándo falla linarith. Cuando hay productos de variables. Es la ocasión para introducir nlinarith y las pistas. Haz explícito que la pista es la idea matemática.
• Errores frecuentes.
  • rw reescribe todas las ocurrencias, no solo la deseada; si hace falta controlar, usa rw [h] at h2 o nth_rewrite.
  • rw falla con «motive is not type correct» o «did not find instance»; casi siempre es un problema de forma sintáctica, no de matemáticas.
  • Alineación de calc.
• Mensaje clave. La automatización cierra pasos obvios; el trabajo humano está en elegir los pasos.

Tema 5. Inducción y recursión

Contenido

Objetivos. Hacer inducción sobre ℕ, trabajar con sumatorios finitos y definir funciones recursivas.

5.1 Inducción. El esquema es el de papel: caso base y paso inductivo.

theorem suma_gauss
  (n : ℕ)
  : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * ∑ i ∈ Finset.range (0 + 1), i = 0 * (0 + 1)
    simp
  | succ k ih =>
    -- k : ℕ
    -- ih : 2 * ∑ i ∈ Finset.range (k + 1), i = k * (k + 1)
    -- ⊢ 2 * ∑ i ∈ Finset.range (k + 1 + 1), i = (k + 1) * (k + 1 + 1)
    rw [Finset.sum_range_succ, mul_add, ih]
    -- ⊢ k * (k + 1) + 2 * (k + 1) = (k + 1) * (k + 1 + 1)
    ring

En succ k ih aparecen k (el valor para el que ya sabemos el resultado) e ih, la hipótesis de inducción. Finset.range (n + 1) es {0, 1, …, n} y Finset.sum_range_succ dice que sumar hasta k+1 es sumar hasta k y añadir el último término.

5.2 Definiciones recursivas.

def fact : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fact n

theorem fact_pos
  (n : ℕ)
  : 0 < fact n :=
by
  induction n with
  | zero =>
    -- ⊢ 0 < fact 0
    simp [fact]
  | succ k ih =>
    -- k : ℕ
    -- ih : 0 < fact k
    -- ⊢ 0 < fact (k + 1)
    show 0 < (k + 1) * fact k
    -- ⊢ 0 < (k + 1) * fact k
    exact Nat.mul_pos (Nat.succ_pos k) ih

#eval fact 5
-- 120

#eval calcula: es la parte «de programación», y aquí sirve solo para comprobar que la definición hace lo esperado (devuelve 120).

Ejercicios.

1. Demuestra por inducción que ∑ i ∈ Finset.range (n + 1), (2 * i + 1) = (n + 1)^2.
2. Define dobla : ℕ → ℕ por recursión y demuestra dobla n = 2 * n.
3. Prueba que fact n ≥ 1 sin usar fact_pos.
4. Reto: 2^n ≥ n + 1 por inducción (pista: omega o nlinarith en el paso).

Consejos didácticos

• Idea clave. La inducción de Lean es literalmente el principio de inducción. Subraya que ih es la hipótesis que en papel escribiríamos «supongamos cierto para k».
• Notación de sumatorios. Los estudiantes se bloquean con Finset. Basta decir que Finset.range n es {0,…,n−1} y que ∑ i ∈ S, f i es la suma de siempre. No hace falta explicar más.
• Errores frecuentes.
  • Confundir n y n + 1 en los casos.
  • Esperar que simp cierre el paso inductivo, cuando suele necesitar el lema de la suma.
  • rw falla porque el objetivo muestra k + 1 + 1 y no k + 2.
• Truco de depuración. Cuando el paso inductivo no sale, pedir que escriban en papel el objetivo y la hipótesis y que se pregunten qué igualdad los une.

Tema 6. Definiciones propias

Contenido

Objetivos. Definir conceptos matemáticos nuevos (propiedades, estructuras) y demostrar enunciados sobre ellos.

6.1 Definir una propiedad. Lean no sabe qué es «inyectiva» en nuestro texto hasta que lo escribimos (Mathlib ya tiene Function.Injective, pero definirlo uno mismo es la mejor forma de entenderlo).

def Inyectiva (f : ℕ → ℕ) : Prop :=
  ∀ a b, f a = f b → a = b

example : Inyectiva (fun n => n + 1) :=
by
  intro a b h
  -- a b : ℕ
  -- h : (fun n => n + 1) a = (fun n => n + 1) b
  -- ⊢ a = b
  simpa using h

Después de intro, h dice (fun n => n + 1) a = (fun n => n + 1) b; simpa simplifica y concluye.

6.2 Límite de una sucesión.

def Converge (a : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - l| < ε

example
  (c : ℝ)
  : Converge (fun _ => c) c :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(fun x => c) n - c| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |(fun x => c) n - c| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ 0
  -- ⊢ |(fun x => c) n - c| < ε
  simpa using hε

Es la definición ε-N de los cursos de Análisis, escrita casi igual. La demostración también sigue el guion de papel: dado ε, elegimos N, y para cada n el valor absoluto es 0 < ε.

6.3 Estructuras. Sirven para agrupar datos.

structure Punto where
  x : ℝ
  y : ℝ

def Punto.norma2 (p : Punto) : ℝ :=
  p.x^2 + p.y^2

theorem Punto.norma2_nonneg
  (p : Punto)
  : 0 ≤ p.norma2 :=
by
  unfold Punto.norma2
  -- ⊢ 0 ≤ p.x ^ 2 + p.y ^ 2
  positivity

6.4 Tipos y universos, solo lo imprescindible. ℕ, ℝ, Set ℕ y ℕ → ℝ son tipos; x : ℕ se lee «x es un elemento de ℕ». Con eso basta. Mathlib usa clases (Group, Field …) para estructuras algebraicas, que se verán de pasada.

Ejercicios.

1. Define Creciente (a : ℕ → ℝ) y demuestra que fun n => (n : ℝ) es creciente.
2. Prueba Converge a l → Converge a l' → l = l' (el límite es único). Es un reto; empieza escribiendo la demostración en papel con ε/2.
3. Define la estructura Racional con numerador y denominador y una función suma. (Solo definir; la demostración de propiedades es opcional.)

Consejos didácticos

• Lo importante. Que el estudiante vea que su vocabulario matemático se traduce literalmente. Los estudiantes de Análisis suelen engancharse aquí.
• Error frecuente. Una definición que parece correcta pero no lo es (por ejemplo, olvidar ε > 0). Lean no avisa: la definición compila. La lección es que Lean verifica demostraciones, no que las definiciones sean las que queríamos.
• Preguntas habituales. «¿Por qué no usar la definición de Mathlib?» Porque aprender a definir es parte del oficio; luego se sustituye por la de Mathlib con Filter.Tendsto y se discute la diferencia.
• Tipos y funciones. Si surgen dudas de teoría de tipos, responder con el lema «un tipo es como un conjunto, con la diferencia de que cada elemento tiene un único tipo».

Tema 7. Moverse por Mathlib

Contenido

Objetivos. Encontrar lemas que no se conocen, leer su enunciado y aplicarlos.

7.1 El problema real. Nadie memoriza Mathlib. La habilidad que se entrena aquí es buscar.

7.2 Herramientas.

#check Nat.add_comm
-- Nat.add_comm (n m : ℕ) : n + m = m + n

example
  (a b : ℕ)
  (hb : 0 < b)
  (h : a ∣ b)
  : a ≤ b :=
by
  exact?

Lean propone Nat.le_of_dvd hb h. La buena práctica es copiar la sugerencia en lugar de dejar exact?.

7.3 Convenciones de nombres. Los nombres de Mathlib son descriptivos: add_comm, mul_pos, sq_nonneg, Finset.sum_range_succ. Con el tiempo se aprende a adivinarlos: a_lt_b_iff suele significar «a < b si y solo si…».

7.4 Trabajar en local. Cuando el estudiante quiere seguir por su cuenta: instalar Lean y VS Code siguiendo las instrucciones oficiales, y crear un proyecto con Mathlib (lake new mi_proyecto math). Para el curso basta con proporcionar una plantilla ya preparada y un procedimiento de arranque escrito, para evitar que alguien se bloquee en la instalación.

Ejercicios.

1. Para cada uno de estos enunciados, encuentra el lema de Mathlib que lo resuelve:
   • 0 < a → 0 < b → 0 < a * b;
   • |a + b| ≤ |a| + |b|;
   • a ≤ b → a ≤ b + c si 0 ≤ c.
2. Usa #check para leer el enunciado de Finset.sum_comm y explica con tus palabras qué dice.
3. Reto: demuestra Nat.Prime 7 de dos maneras (norm_num y decide).

Consejos didácticos

• Objetivo pedagógico. Desmitificar. Que el estudiante entienda que buscar el lema es parte normal del trabajo, igual que consultar un teorema en un libro.
• Instalación. Si se hace en local, reserva una sesión aparte y acompaña de cerca. Es el punto donde más estudiantes se pierden. Una plantilla compartida ahorra horas.
• Errores frecuentes.
  • Dejar exact? en la entrega: es lento y no es una demostración estable.
  • Los nombres genéricos (add_comm) funcionan para varios tipos; si el estudiante da un tipo incorrecto, Lean se queja con mensajes largos. Enseña a leer primero la última línea del error.
• Buenas prácticas. Guardar con frecuencia, comentar con --, partir demostraciones largas en lemas auxiliares con nombre.

Tema 8. Proyecto final

Contenido

Objetivo. Formalizar un resultado elemental completo y presentarlo.

Opciones de proyecto (a elegir una).

1. Teoría de conjuntos. Leyes de De Morgan y distributividad para conjuntos y familias de conjuntos.
2. Aritmética. Suma de los n primeros impares, fórmula de Gauss, desigualdad de Bernoulli.
3. Análisis. Unicidad del límite y límite de la suma de dos sucesiones convergentes con la definición ε-N del Tema 6.
4. Álgebra. En un grupo, unicidad del neutro y del inverso, usando Group de Mathlib.
5. Libre. Una proposición de un curso que el estudiante esté siguiendo, acordada con el docente.

Entregables. Un archivo .lean sin sorry, con comentarios que expliquen la estrategia, más una página con la demostración en papel y una reflexión breve sobre qué costó más en Lean.

Consejos didácticos

• Qué valorar.
  1. Que compile.
  2. Que los enunciados sean fieles al texto matemático.
  3. Que la estructura (lemas auxiliares) sea clara.
  4. Que el estudiante sepa explicar su propia demostración.
• Consejo. Obliga a escribir primero la demostración en papel dividida en lemas; la versión en Lean es la traducción. Los proyectos que se improvisan directamente en Lean acaban en frustración.
• Extensiones. Para grupos avanzados: topología básica, teoría de Galois en pequeño, o contribuir un lema pequeño a Mathlib.

Apéndice A. Chuleta de tácticas

Apéndice B. Cómo leer un error

1. Lee primero la línea marcada en rojo, no el mensaje completo.
2. «unsolved goals» significa que la demostración no ha terminado: mira qué objetivo queda.
3. «type mismatch» indica que has dado algo que no encaja con el objetivo: compara los dos tipos.
4. «unknown identifier» suele ser un error ortográfico o un import que falta.
5. Si no entiendes el mensaje, pon sorry en el paso, comprueba que el resto compila y avanza.

Apéndice C. Recursos

• The Natural Number Game (Kevin Buzzard): puerta de entrada lúdica, perfecta como actividad previa al Tema 1.
• The mechanics of proof (Heather Macbeth): introducción de Lean para matemáricos.
• Mathematics in Lean (Avigad y Massot): el texto interactivo de referencia para matemáticos, ideal como lectura complementaria.
• Repositorio Formalising Mathematics (Imperial College London).
• Theorem Proving in Lean 4: más técnico, útil para entender el trasfondo de tipos.
• Archivo 100 Theorems in Lean (referencia de dificultad realista).
• La documentación de Mathlib y el foro Zulip de Lean para consultas.

Apéndice D. Sugerencias de calendario

• Curso corto (4 sesiones). Temas 1, 2, 3 y 4, con un miniproyecto sobre conjuntos.
• Curso estándar (8 sesiones). Un tema por sesión, con el proyecto final como trabajo de la última semana.
• Curso intensivo (2 días). Mañana: Temas 1 a 3. Tarde: Temas 4 y 5. Segundo día: Temas 6 y 7, y mini-proyecto en grupos.