Nivel 0 · ¿Por qué verificar?

El problema de la confianza

Durante más de un siglo, la fiabilidad de una demostración matemática ha descansado en la revisión por pares: un argumento se acepta cuando una comunidad de expertos se convence de su corrección. El mecanismo ha sido enormemente fructífero, pero tiene límites conocidos, y ambos se agudizan conforme las demostraciones crecen en tamaño y complejidad. Hay pruebas demasiado largas o técnicas para revisarse con certeza, y hay errores que sobreviven años en la literatura. Esta página examina un ejemplo de cada límite y presenta la salida que estudia todo este sitio: los asistentes de pruebas.

Pruebas que ningún revisor puede leer

La demostración del teorema de los cuatro colores publicada en los años setenta causó una revolución en la matemática, porque no fue una prueba que involucrara solo matemática tradicional: partes esenciales del argumento consistieron en la ejecución de un programa de computadora que examinó innumerables casos específicos. Ningún revisor humano podía inspeccionar esa porción del razonamiento. Aceptar el teorema exigía confiar en programas escritos para la ocasión, además del texto matemático que los rodeaba.

En 2005 la historia tomó un rumbo distinto. Georges Gonthier (Microsoft Research, Cambridge), en colaboración con Benjamin Werner (École Polytechnique), formalizó la prueba en el asistente Coq: 60,103 líneas de código en 132 archivos, que reutilizan aproximadamente un tercio de la versión original. La diferencia decisiva frente a los intentos anteriores no es el volumen, sino la arquitectura de la confianza: la nueva prueba no usó múltiples programas de computadora para verificar casos particulares, sino que todo el argumento, incluida su parte computacional, fue comprobado por el núcleo (kernel) de Coq (Gonthier, 2008) . En lugar de confiar en una colección heterogénea de programas, basta confiar en un único verificador pequeño.

Enunciados que sobreviven décadas

El segundo límite es más incómodo: afirmaciones que la comunidad da por buenas durante mucho tiempo. Un ejemplo clásico es la conjetura de Mertens. Sea $\mu$ la función de Möbius y $M(n) = \sum_{k \le n} \mu(k)$. Mertens conjeturó en 1897 que $|M(n)| < \sqrt{n}$ para todo $n > 1$; Stieltjes había anunciado ya en 1885 una demostración de un enunciado análogo, demostración que nunca publicó. La conjetura tenía a su favor una verificación numérica masiva, para miles de millones de valores de $n$, y de haber sido cierta habría implicado la hipótesis de Riemann. En 1985, Odlyzko y te Riele demostraron que es falsa. La refutación, además, no exhibe contraejemplo alguno: demuestra que existe uno, sin poder señalarlo. Ni un siglo de convicción colectiva ni la evidencia numérica, por abrumadora que sea, sustituyen a una demostración.

Qué es un asistente de pruebas

Un asistente de pruebas es un programa en el que cada paso de un razonamiento se verifica de forma mecánica contra un núcleo lógico pequeño y de confianza. El matemático sigue escribiendo la demostración; lo que cambia es el criterio de aceptación: una prueba aceptada deja de depender de la atención de un revisor humano, porque ningún paso puede omitirse ni darse por «evidente» sin que el núcleo lo compruebe. La confianza no desaparece, se concentra: en lugar de repartirse entre revisores, programas auxiliares y tradición, recae en un verificador único y deliberadamente minúsculo, que puede estudiarse con un cuidado imposible de dedicar a cada demostración individual.

El costo conviene decirlo desde el principio: traducir un cuerpo de conceptos matemáticos a un asistente de pruebas es un trabajo arduo. La contrapartida es que, una vez hecho, queda una biblioteca de código que otros investigadores pueden ampliar y usar para definir objetos de nivel superior, y que permite verificar pruebas que de otro modo serían extremadamente laboriosas, quizá prácticamente imposibles, de comprobar por un humano.

La promesa, en dos resultados concretos

Este sitio adapta una tesis que estudia el asistente Lean 4 con un doble propósito: entender por qué funciona (qué teoría matemática lo sostiene) y usarlo para verificar resultados concretos. La promesa no se argumenta en abstracto; se exhibe con dos estudios de caso formalizados por completo, elegidos como dos extremos de un mismo espectro:

1. Un teorema de lógica. La completitud de la deducción natural clásica proposicional, es decir, que toda tautología es un teorema, demostrada de manera interna mediante una realización constructiva del lema de Kalmár .
2. Un algoritmo. La corrección del algoritmo quicksort, separada en sus dos mitades independientes: que la salida es una permutación de la entrada y que está ordenada.

En ambos se impone la misma disciplina de rigor: no se admite ninguna laguna (la palabra clave sorry, con la que Lean permite posponer una prueba, no aparece ni una sola vez), no se postula ningún lema sin demostración, y el resultado final se somete a una auditoría de axiomas que expone con exactitud los supuestos sobre los que descansa. Qué es Lean, qué significa exactamente «verificado» y por qué esa auditoría es el mecanismo de honestidad del método se tratan en la tercera página de este módulo. Antes conviene ver de dónde viene la idea misma de formalizar: es una historia de más de un siglo.