Nivel 0 · ¿Por qué verificar?

Un siglo de formalización

La idea de que una máquina compruebe demostraciones no nació con las computadoras. Es el último episodio de un programa mucho más antiguo: construir un lenguaje en el que el razonamiento matemático quede tan explícito que su corrección pueda decidirse por inspección puramente sintáctica. Esta página recorre ese arco, desde la lógica del siglo XIX hasta los asistentes de pruebas actuales, siguiendo el capítulo de contexto histórico de la tesis.

Frege, Russell y el nacimiento de los tipos

El punto de partida habitual es el Begriffsschrift de Gottlob Frege (1879), una «escritura conceptual» concebida como lenguaje de fórmulas libre de expresiones retóricas, que sustituyó la pareja sujeto-predicado por la de función y argumento. El tratado sentó las bases de la lógica moderna y de la teoría de los cuantificadores. En 1902, sin embargo, Bertrand Russell escribió a Frege comunicándole una paradoja de su sistema (la hoy llamada paradoja de Russell), que mostraba un problema fundamental en la teoría básica de conjuntos, ligado a la autorreferencia. La respuesta de Russell y Alfred North Whitehead fue Principia Mathematica (tres volúmenes, 1910-1913): derivar las verdades de la matemática a partir de un conjunto bien definido de axiomas y reglas de inferencia, empleando una teoría ramificada de tipos para bloquear las paradojas. Ahí aparece, con propósito inicialmente defensivo, la noción de tipo que un siglo después sería el corazón de los asistentes de pruebas.

El programa de Hilbert y la respuesta de Gödel

Hacia 1918, David Hilbert se concentró en el problema de la independencia (entender las relaciones lógicas entre los axiomas de una teoría, probando que cierta proposición no es derivable de axiomas dados) y, después, en el problema de la consistencia, ligado al concepto de infinito. Aunque su trabajo suele etiquetarse como «formalismo», su enfoque real estaba en las operaciones finitistas: los conceptos transfinitos debían usarse como herramientas de representación, no como ingredientes esenciales de las pruebas. Para la década de 1930, el programa de Hilbert buscaba reducir todo razonamiento matemático a métodos finitistas. Los teoremas de incompletitud de Gödel demostraron las limitaciones de ese programa: no todas las verdades de la matemática pueden derivarse de un único conjunto consistente de axiomas.

Conviene precisar qué quedó refutado y qué no. La incompletitud acota lo que un sistema formal puede demostrar; no toca la tarea, más modesta, de comprobar mecánicamente si una derivación dada es correcta. Esa segunda tarea es exactamente la que realizan los asistentes de pruebas.

1936: Church y el cálculo lambda

En la década de 1930, Alonzo Church desarrolló el cálculo lambda no tipado, un hito en la formalización del concepto de computabilidad. En 1936 introdujo la λ-definibilidad, un sistema formal que precisa qué significa que una función sea computable (Church, 1936) , y demostró que esta noción es equivalente a la Turing-computabilidad, presentada por Alan Turing mediante su máquina abstracta: cualquier cálculo realizable por una máquina de Turing puede llevarse a cabo dentro del cálculo lambda. La notación es deliberadamente austera: en lugar de escribir una función como $x^3 + 1$, se escribe $\lambda x.\, x^3 + 1$, donde $\lambda$ marca la abstracción de la variable $x$. Se considera que Church sentó las bases de varias ramas de la computación teórica e influyó en la creación de los lenguajes de programación funcional (Nederpelt y Geuvers, 2014) .

AUTOMATH: el primer asistente de pruebas

A finales de los años sesenta, N. G. de Bruijn inició el proyecto Automath, con el objetivo de crear una versión completamente formal de las expresiones de la matemática, verificable por una computadora y relativamente cercana a cómo los matemáticos suelen comunicarse. En 1967 presentó un primer lenguaje formal (PAL, el Lenguaje Automático Primitivo) y en 1968 su extensión, el Automath básico, después llamado AUT-68. El proyecto, dirigido por de Bruijn hasta principios de los años ochenta, demostró que la verificación automática de la matemática era posible, aunque pasaron décadas antes de que ese trabajo pionero fuera aceptado del todo entre los investigadores. A Automath se le considera el primer asistente de pruebas.

Martin-Löf: proposiciones como conjuntos de pruebas

En los mismos años surgieron varios formalismos para la construcción de programas, entre ellos la teoría de tipos intuicionista de Per Martin-Löf, presentada en 1971. La teoría proporciona un marco para expresar tanto las especificaciones de los programas como los programas mismos, y garantiza la terminación de los programas bien tipados. Su rasgo más influyente es semántico: las proposiciones se interpretan como conjuntos cuyos elementos son sus pruebas, de modo que una proposición falsa corresponde a un conjunto vacío y una verdadera a uno habitado. Para 1979, Martin-Löf había extendido su teoría a una forma polimórfica, estableciendo la conexión entre la matemática y la computación. Esta identificación de proposiciones con tipos es la semilla de la correspondencia de Curry–Howard que organiza todo lo que sigue en este sitio.

1984: el Cálculo de Construcciones

En 1984, en la conferencia internacional sobre tipos celebrada en Francia, Thierry Coquand y Gérard Huet presentaron un trabajo sobre tipos dependientes y polimorfismo que extendía la teoría constructiva de Martin-Löf hacia el sistema Automath: el Cálculo de Construcciones (Coquand y Huet, 1988) . En su tesis doctoral, Coquand dio el análisis metateórico y demostró la terminación y el fundamento lógico de la teoría. El CoC fue la base del sistema de pruebas del proyecto Formel, cuya primera etapa dio origen al sistema Coq; con las contribuciones posteriores de Coquand (un algoritmo de síntesis de pruebas de estilo secuencial) y de Christine Mohring (un algoritmo de búsqueda de pruebas) se llegó en 1988 al Cálculo de Construcciones Inductivas , la teoría que Lean implementa hoy.

Los asistentes en la práctica

Con la teoría madura, los resultados llegaron. En 2005, Georges Gonthier y Benjamin Werner formalizaron en Coq la prueba del teorema de los cuatro colores, comprobada íntegramente por el núcleo del sistema (Gonthier, 2008) . La verificación saltó además de los teoremas al software crítico: CompCert es un compilador de C cuya corrección está demostrada formalmente (Leroy, 2023) . En Isabelle/HOL, Lawrence Paulson mecanizó los dos teoremas de incompletitud de Gödel, incluida la primera prueba automatizada del segundo, detectando de paso errores en la literatura existente. En 2013, Leonardo de Moura inició Lean en Microsoft Research, buscando una plataforma de prueba de teoremas más accesible y eficiente, con capacidades de automatización poderosas (Avigad et al., 2015) . Y en la matemática de frontera: Peter Scholze y Dustin Clausen introdujeron en 2019 la matemática condensada, y uno de sus teoremas más intrincados fue verificado con éxito en Lean por un equipo liderado por Johan Commelin, en el proyecto llamado «Liquid Tensor Experiment».

De la crónica a la teoría

El hilo que va del cálculo lambda de Church a la teoría de tipos de Martin-Löf y al Cálculo de Construcciones de Coquand y Huet no es solo cronología: es exactamente el orden conceptual de los módulos que siguen. La historia dice que la verificación mecánica funciona; para entender por qué funciona (por qué comprobar una demostración puede reducirse a un cálculo sintáctico), hay que empezar por el cálculo lambda. El nivel 1 lo hace desde cero: términos, variables libres, sustitución y β-reducción.