Introducción
Casi toda la matemática moderna se escribe en el lenguaje de la Teoría de Conjuntos, pero casi toda la matemática verificada por computadora se hace en Teoría de Tipos. ¿Por qué existe esta discrepancia? La respuesta está en como las asignaciones de verdad y las demostraciones dependen mucho de un marco.
Dentro del estudio de la lógica matemática, cuyo punto de partida busca responder a la pregunta: ¿Cómo se razona y deduce correctamente?, se debe enfatizar dos enfoques: la sintaxis y la semántica.
La lógica sintáctica
Ésta provee métodos para estudiar sistemas formales para fundamentar una teoría matemática. Para generar un sistema formal, lo primero es construir un vocabulario y un conjunto de expresiones bien formadas, el lenguaje de la teoría. Después, se construye las reglas de inferencia, cuyo objetivo es, a través de ciertas expresiones bien formadas que se considerarán en el inicio de la teoría, denominados axiomas, obtener nuevas expresiones llamadas proposiciones.
Al conjunto de la aplicación sucesiva de reglas de inferencias, expresiones bien formadas y axiomas que permiten obtener una nueva proposición se le conoce como demostración de la proposición. Desde este punto de vista, una demostración es solo un camino para obtener una proposición a través de otras, y los axiomas son el punto de partida. Aquí no se pregunta sobre su veracidad, aunque a priori estos sistemas formales se construyen asumiendo que son verdades dentro de un marco de estudio. Su objetivo de estudio se puede considerar en palabras sencillas como la correcta ejecución de la deducción.
La lógica semántica
A diferencia de la sintaxis, que se preocupa por la forma, la semántica se ocupa del significado y la interpretación. Su objetivo es estudiar la relación entre el lenguaje formal y las estructuras matemáticas que este describe; formalmente, esto se conoce como Teoría de Modelos. Aquí, la pregunta central no es si una expresión se puede derivar, sino ¿bajo qué condiciones una proposición es verdadera?
Para responderla, se asigna una interpretación a los símbolos del vocabulario: las constantes se vuelven objetos concretos, y los predicados se vuelven relaciones en un conjunto específico (el universo del modelo). Se dice que una estructura es un modelo de una teoría si todos los axiomas de dicha teoría son verdaderos bajo esa interpretación. Desde este punto de vista, la verdad no es una propiedad intrínseca de los símbolos, sino una correspondencia entre la proposición y la estructura matemática que modela. Su objetivo final es garantizar que lo que demostramos sintácticamente (lo deducible) corresponda fielmente con lo que es verdadero en los modelos matemáticos (lo válido).
Ambos enfoques constituyen una formación acertada a una teoría matemática con bases sólidas. También, esta distinción plantea una cuestión: idealmente, quisiéramos que todo lo que es verdadero en nuestros modelos matemáticos pudiera ser demostrado mediante las reglas sintácticas, conocido como Completitud, y que todo lo demostrado sea efectivamente verdadero.
Si las demostraciones sintácticas son simplemente manipulaciones finitas de símbolos siguiendo reglas predefinidas, surge una pregunta natural:
¿Existe un algoritmo capaz de decidir mecánicamente la veracidad o falsedad de cualquier proposición matemática?
Esta interrogante histórica fue estudiado dentro de la Teoría de la Computabilidad. Para responderla, primero fue necesario definir formalmente qué significa calcular o seguir un algoritmo.
Para ilustrar esta dualidad entre forma y significado, consideremos brevemente la Lógica Proposicional. Desde la perspectiva sintáctica, definimos un alfabeto y reglas de formación para construir expresiones bien formadas. A partir de axiomas puramente estructurales, como $\varphi \to (\psi \to \varphi)$, y reglas de inferencia como el Modus Ponens, podemos derivar mecánicamente teoremas, por ejemplo, el principio del tercero excluido $P \lor \neg P$ (definiendo la disyunción en términos de implicación y negación). Por otro lado, la perspectiva semántica verifica esta misma proposición mediante tablas de verdad, asignando valores en $\{0,1\}$ para confirmar que la sentencia es una tautología ($\vDash P \lor \neg P$). En este sistema simple, la sintaxis y la semántica coinciden armoniosamente.
Sin embargo, la distinción se vuelve crítica y la intuición mecánica se desafía al ascender a la Lógica de Primer Orden. Considere, por ejemplo, la sentencia sintácticamente correcta:
$$\varphi \equiv \exists x (x \cdot x + 1 = 0)$$¿Es $\varphi$ verdadera? La sintaxis por sí sola no puede responder. La verdad de Tarski nos exige un modelo: si interpretamos el universo como los números reales, entonces $\mathbb{R} \not\vDash \varphi$; pero si nuestro modelo son los números complejos, entonces $\mathbb{C} \vDash \varphi$.
Esto evidencia que la verdad matemática a menudo depende de la estructura semántica subyacente, mientras que la demostración busca ser un proceso finito e independiente de dicha interpretación.
Esta tensión histórica desembocó en preguntas fundamentales sobre la decidibilidad. Si todo lo verdadero fuera demostrable mecánicamente, podríamos reducir la matemática a un cálculo. Un ejemplo paradigmático de esta ambición fue el Décimo Problema de Hilbert. Sea $P$ un polinomio con coeficientes enteros y consideremos la proposición:
$$\Psi := \exists x_1 \dots \exists x_n [ P(x_1, \dots, x_n) = 0 ]$$Hilbert buscaba idear un proceso —un algoritmo finito— que pudiera determinar si tal ecuación tiene solución en los números enteros; es decir, decidir mecánicamente si $\mathbb{N} \vDash \Psi$.
Para responder si tal proceso existe, o más generalmente, para determinar los límites de lo que puede ser demostrado (computado) sintácticamente frente a lo que es verdadero semánticamente, fue imperativo formalizar matemáticamente el concepto intuitivo de proceso o cálculo.
Cálculo Lambda
Un algoritmo es un procedimiento sistemático para resolver un problema mediante una secuencia finita de pasos discretos. En el contexto lógico, debe satisfacer:
- Finitud y Determinismo: Descripción finita y pasos unívocamente determinados.
- Manipulación de Símbolos: Opera sobre datos discretos (fórmulas, números).
Esta noción intuitiva se formalizó matemáticamente a través de modelos equivalentes como las Máquinas de Turing, las Funciones Recursivas y el Cálculo Lambda. Este último modelo es fundamental para nosotros, ya que establece la conexión directa entre computar una función y demostrar un teorema.
El cálculo lambda, introducido por Alonzo Church, es un sistema formal diseñado para investigar la definición de función, la aplicación de funciones y la recursión. En Lean, las demostraciones son, en última instancia, términos de este cálculo. A diferencia de la teoría de conjuntos, aquí construimos términos inductivamente a partir de un conjunto infinito de variables $\mathcal{V} = \{x, y, z, \dots\}$.
- Variables: Si $x \in \mathcal{V}$, entonces $x \in \Lambda$.
- Abstracción: Si $x \in \mathcal{V}$ y $M \in \Lambda$, entonces $(\lambda x. M) \in \Lambda$.
- Aplicación: Si $M, N \in \Lambda$, entonces $(M N) \in \Lambda$.
La computación en este sistema se define estrictamente como reglas de reescritura de texto. La regla principal es la $\beta$-reducción, que formaliza la noción de sustitución. Sea $M[x := N]$ el resultado de sustituir todas las ocurrencias libres de la variable $x$ en $M$ por el término $N$.
Un concepto crítico para los asistentes de pruebas es el de Forma Normal. Se dice que un término está en forma normal si no se le pueden aplicar más $\beta$-reducciones. Computar en Lean consiste, esencialmente, en reducir términos hasta alcanzar su forma normal para verificar si dos expresiones son definicionalmente iguales.
Una vez definida la reducción y la forma normal, podemos formalizar qué significa que dos términos sean lo mismo en esta teoría. A diferencia de la igualdad proposicional (que se debe demostrar), existe una noción más primitiva de igualdad que el sistema verifica mecánicamente.
Esta definición concreta la noción de significado dentro de la teoría: el significado de un término es su forma normal.
- En la teoría de conjuntos, para verificar $2 + 2 = 4$ requerimos axiomas aritméticos y lógica de primer orden.
- En la teoría de tipos, $2 + 2$ es simplemente una notación para un término que, al aplicar las reglas de $\beta$-reducción, se transforma sintácticamente en $4$. Por tanto, $2 + 2 \equiv 4$ es una identidad sintáctica verificable por un algoritmo, no un teorema que requiere demostración.
Esto tiene una consecuencia inmediata para el sistema Lean: verificar una demostración es, en gran medida, verificar igualdades definicionales. Si el usuario afirma que un término $p$ es una prueba de una proposición $P$, el sistema verifica si el tipo de $p$ reduce a la misma forma normal que $P$. Por lo tanto, en este sistema, la sintaxis equipada con reglas de reducción constituye su propia semántica. Si dos términos reducen a la misma forma normal, son, para todos los efectos matemáticos dentro de la teoría, el mismo objeto.
Ejemplo (Reducción paso a paso): Consideremos el término $(\lambda x. x) a$. Al aplicar la reducción, sustituimos $x$ por $a$ en el cuerpo:
$$(\lambda x. x) a \longrightarrow_\beta x[x:=a] = a$$
Acerca de la Teoría de Tipos
El $\lambda$-cálculo puro es demasiado expresivo: permite construir términos que nunca alcanzan una forma normal (bucles infinitos), lo cual en lógica correspondería a inconsistencias. Para evitar esto, la Teoría de Tipos se monta sobre el cálculo lambda como un sistema de reglas deductivas que filtra los términos válidos.
Para formalizar este filtro, la Teoría de Tipos introduce un cambio de paradigma respecto a la Teoría de Conjuntos. En conjuntos, la pertenencia es una proposición: dado un objeto $x$ y un conjunto $S$, la afirmación “$x \in S$” puede ser verdadera o falsa e incluso indecidible. En cambio, en la Teoría de Tipos, la pertenencia es un juicio sintáctico estático.
En este marco, introducimos el juicio de tipado $a : A$, que se lee “$a$ es un término de tipo $A$”. A continuación definimos los tipos fundamentales mediante sus reglas de formación, introducción, eliminación y computación.
- Formación: $A \to B$ es un tipo.
- Introducción ($\lambda$-abstracción): Si asumiendo $x:A$ podemos construir un término $\Phi:B$, entonces la abstracción $\lambda x. \Phi$ tiene tipo $A \to B$.
- Eliminación (Aplicación): Si $f : A \to B$ y $a : A$, entonces $f(a) : B$.
- Computación: $(\lambda x. \Phi)(a) \equiv \Phi[x := a]$.
Esta formalización revela una identidad estructural profunda entre la Lógica (Deducción Natural) y la Programación (Teoría de Tipos). Antes de enunciarla, necesitamos definir formalmente el entorno donde ocurren las deducciones.
El isomorfismo de Curry-Howard establece que las reglas de inferencia lógica son isomorfas a las reglas de construcción de tipos. Observemos el paralelismo para la implicación:
| Lógica: Implicación | Tipos: Funciones |
|---|---|
| Introducción ($\implies$) | Abstracción ($\lambda$) |
| $\displaystyle \frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}$ | $\displaystyle \frac{\Gamma, x:A \vdash t:B}{\Gamma \vdash \lambda x.t : A \to B}$ |
| Eliminación (Modus Ponens) | Aplicación |
| $\displaystyle \frac{\Gamma \vdash A \to B \quad \Gamma \vdash A}{\Gamma \vdash B}$ | $\displaystyle \frac{\Gamma \vdash f : A \to B \quad \Gamma \vdash a : A}{\Gamma \vdash f(a) : B}$ |
Bajo esta correspondencia:
- Una proposición $P$ es vista como un Tipo.
- Una demostración de $P$ es un Programa $p$ tal que $p : P$.
- Verificar una prueba es verificar que el programa compile (Type Checking).
La expresividad de Lean proviene de generalizar las funciones y los productos pares para permitir que los tipos dependan de valores, capturando así los cuantificadores lógicos.
- Introducción: Un término es una función $\lambda x. t$ tal que para cada entrada $a:A$, el resultado tiene tipo $P(a)$.
- Eliminación: La aplicación $f(a)$ devuelve un valor de tipo $P(a)$.
- Introducción: Un elemento es un par dependiente $\langle a, b \rangle$ donde $a:A$ y $b:P(a)$.
- Eliminación: Proyecciones para recuperar el testigo $a$ y la prueba $b$.
Ejemplo: La Identidad y la Tautología Trivial
Sea $A$ un tipo cualquiera. Buscamos un término del tipo $A \to A$.
- Perspectiva Lógica ($A \implies A$): Queremos demostrar que “si $A$ es verdad, entonces $A$ es verdad”. Usando las reglas de inferencia, asumimos $x:A$ y trivialmente concluimos $x:A$.
- Perspectiva Computacional (Algoritmo): Buscamos un procedimiento que reciba un dato de tipo $A$ y devuelva un dato de tipo $A$. El algoritmo minimal es la función identidad.
Formalmente: $\mathsf{id}_A :\equiv (\lambda x. x) : A \to A$. En Lean:
example : A -> A := fun x => x
Ejemplo: Composición y Transitividad
Sean $A, B, C$ tres tipos. Buscamos un término del tipo $(A \to B) \to (B \to C) \to (A \to C)$.
- Perspectiva Lógica: Corresponde a la transitividad de la implicación (Silogismo Hipotético).
- Perspectiva Computacional: Describe la composición de funciones $g \circ f$.
Formalmente: $\mathsf{comp} :\equiv \lambda f. \lambda g. \lambda x.\ g(f(x))$. En Lean:
example : (A -> B) -> (B -> C) -> (A -> C) := fun f g x => g (f x)
Matemáticas en Lean
Hasta este punto, hemos establecido que una demostración matemática es formalmente un término bien tipado en el $\lambda$-cálculo. Sin embargo, para un matemático en ejercicio, construir estos términos “a mano” resultaría una tarea tediosa.
Lean resuelve esta dificultad mediante una sintaxis expresiva que mimetiza la notación estándar y un sistema de metaprogramación táctica.
En cuanto a la sintaxis, Lean introduce una distinción semántica:
- Datos (
def): Objetos con contenido computacional relevante (funciones, números). - Proposiciones (
theorem/lemma): Verdades lógicas donde rige el principio de Irrelevancia de Pruebas.
| Concepto Teórico | Notación Matemática | Sintaxis en Lean 4 |
|---|---|---|
| Juicio de Tipado | $a \in A$ ó $a : A$ | a : A |
| $\lambda$-Abstracción | $\lambda x. t$ | fun x => t |
| Tipo Función | $A \to B$ | A -> B |
| Cuantificador Universal | $\forall x \in A, P(x)$ | forall x : A, P x |
| Implicación | $P \implies Q$ | P -> Q |
| Aplicación | $f(x)$ | f x |
La innovación fundamental es el Modo Táctico. Al utilizar la palabra clave by, el usuario entra en un modo donde escribe instrucciones para que Lean construya el término. La pantalla muestra el Estado Táctico:
- El Contexto Local ($\Gamma$): Variables e hipótesis disponibles.
- El Objetivo ($\vdash$ Target): La proposición a demostrar.
Tácticas comunes
intro(Configuración del contexto): Desempaqueta “Sea $x \in A$” o “Supongamos $P$”, moviendo variables al contexto local.apply(Razonamiento hacia atrás): Si queremos probar $Q$ y tenemos un lema $P \implies Q$,applycambia el objetivo a $P$.rw(Manejo de igualdades): Sustituye términos equivalentes.rw [h]busca el lado izquierdo de la igualdadhy lo reemplaza.obtain,use,cases(Existenciales y Descomposición):obtainextrae testigos de existenciales ($\exists_E$),useprovee testigos ($\exists_I$), ycasesdivide conjunciones o disyunciones.exact(El cierre): Verifica que un término tenga exactamente el tipo del objetivo, cerrando la prueba.
Ejemplo Práctico: Conjuntos e Imágenes
Aplicaremos todo lo aprendido traduciendo un teorema estándar de Teoría de Conjuntos.
Demostración Matemática: Sea $x\in f(f^{-1}(Y))$, entonces $\exists y\in f^{-1}(Y)$ tal que $x=f(y)$. Pero por definición de imagen inversa, se tiene $f(y)\in Y$. Sustituyendo, obtenemos $x\in Y$. Conversamente, sea $x \in Y$. Como $f$ es sobreyectiva, existe $y\in \alpha$ tal que $f(y)=x$. Esto implica que $f(y) \in Y$, es decir, $y \in f^{-1}(Y)$. Por lo tanto, $x = f(y) \in f[f^{-1}[Y]]$.
En Lean 4:
En Lean 4, importamos la librería de conjuntos y declaramos el enunciado:
import Mathlib.Data.Set.Image
import Mathlib.Tactic
open Set Function
theorem image_preimage_of_surjective
{alpha beta : Type} (f : alpha -> beta)
(h_surj : Surjective f) (Y : Set beta) :
f '' (f ⁻¹' Y) = Y := by
A continuación, la demostración paso a paso. Nótese en el paso 7 el uso de mem_preimage para ajustar la sintaxis antes de reescribir.
| Razonamiento Matemático | Código en Lean (Tácticas) |
|---|---|
| 1. Para demostrar la igualdad de conjuntos, probamos la doble implicación ($y \in A \iff y \in B$) para un $y$ arbitrario. | ext yconstructor |
| Dirección 1 ($\to$): Sea $y \in f[f^{-1}[Y]] \implies y \in Y$ | |
| 2. Desempaquetamos la hipótesis de imagen: existe un $x$ en la preimagen tal que $f(x) = y$. | intro hobtain ⟨x, h_preim, h_eq⟩ := h |
| 3. Sustituimos $y$ por $f(x)$ (usando la igualdad invertida). Como $x$ está en la preimagen, $f(x) \in Y$, lo que cierra la prueba. | rw [← h_eq]exact h_preim |
| Dirección 2 ($\leftarrow$): Sea $y \in Y \implies y \in f[f^{-1}[Y]]$ | |
| 4. Asumimos la hipótesis $y \in Y$. | intro hy |
| 5. Usamos la sobreyectividad de $f$: existe un $x$ tal que $f(x) = y$. | obtain ⟨x, h_eq⟩ := h_surj y |
| 6. Proponemos este $x$ como el elemento cuya imagen es $y$. Reescribimos el objetivo para buscar $f(x)$ en lugar de $y$. | rw [← h_eq]use x |
| 7. Debemos probar: a) $x \in f^{-1}[Y]$. Por definición esto es $f(x) \in Y$. Reescribimos $f(x)$ como $y$ y usamos la hipótesis original. b) $f(x) = f(x)$ (trivial). |
constructor· rw [mem_preimage] rw [h_eq] exact hy· rfl |
6. Acerca del papel de las demostraciones, la IA y el matemático
La formalización de demostraciones mediante la lógica de Teoría de Tipos ha propiciado el desarrollo de software especializado para la comprobación de pruebas. Más recientemente, el auge de los Grandes Modelos de Lenguaje (LLM) ha introducido una herramienta con inmensas posibilidades para la investigación. No obstante, es crucial considerar ciertos matices técnicos y filosóficos.
Resultados fundamentales de la teoría de la Computabilidad, como el Problema de la Parada de Turing o los Teoremas de Incompletitud de Gödel, demuestran que en las matemáticas no existe un algoritmo general para decidir la verdad de cualquier proposición, ni todo es demostrable en un sistema formal con aritmética consistente. Esto implica la imposibilidad teórica de crear una automatización que obtenga todas las respuestas matemáticas de manera autónoma.
Bajo esta luz, el rol del matemático no desaparece, sino que se transforma. Como señala el Dr. Terence Tao, esta evolución ofrece la oportunidad de transitar de una matemática artesanal —donde el investigador debía mantener la totalidad de la prueba en su mente— a una matemática industrial. En este nuevo paradigma, el matemático actúa como un comandante de alto nivel que define la estrategia (por ejemplo: “utiliza teoría de Hodge $p$-ádica para conectar con este resultado”), mientras que la IA intenta completar los detalles tácticos. Si la máquina se atasca debido a la complejidad o indecidibilidad, la intuición humana debe intervenir para proveer los “lemas puente” necesarios.
Sin embargo, esta potencia conlleva un riesgo que Tao denomina el Problema de la Especificación o la “trampa semántica”. Una inteligencia artificial verifica la validez sintáctica (¿se sigue $B$ de $A$?), pero es incapaz de verificar la validez semántica (¿es $A$ lo que realmente queríamos definir?). Si se formaliza una declaración con errores sutiles —como olvidar una condición de contorno en una variedad—, la IA podría generar una demostración correcta de un teorema inútil sobre un objeto “roto”.
Así, el matemático se consolida como el arquitecto que diseña los planos (definiciones y enunciados), mientras que la IA opera como el albañil que coloca los ladrillos lógicos.
Finalmente, la indecidibilidad de Turing implica que el territorio matemático es infinito y accidentado; no existe un mapa automático. Si bien la IA es excelente para responder a la pregunta “¿Es cierto $X$?”, carece todavía de la capacidad para discernir “¿Es $X$ interesante?”. El valor del investigador se desplazará hacia la formulación de las preguntas correctas y la definición de nuevas estructuras fértiles —como lo hizo Peter Scholze con los espacios perfectoides—. En consecuencia, se requiere que el matemático actual potencie su creatividad y liderazgo; habilidades que, elevadas a un nivel industrial, permitirán definir las estructuras del futuro.
Nota sobre Lean: Lean es excepcionalmente fuerte en Teoría de Categorías en comparación con otros asistentes de pruebas (como Coq o Isabelle).