Nivel 0 · ¿Por qué verificar?

Qué es Lean y qué promete

Un asistente entre varios

Lean es un asistente de pruebas iniciado por Leonardo de Moura en Microsoft Research en 2013, con el propósito de ofrecer una plataforma de prueba de teoremas más accesible y eficiente que las existentes (Avigad et al., 2015) . Lean 4 es la versión actual, y es la que usa la tesis que este sitio adapta. Hoy conviven varios asistentes maduros (Coq, Isabelle/HOL y Agda, entre otros), y la elección de Lean responde a razones concretas, no a una pretensión de superioridad: su biblioteca Mathlib es una de las más extensas y activas, lo que permite disponer de definiciones estándar (órdenes, listas, permutaciones) ya formalizadas; su núcleo de verificación es pequeño; la orden #print axioms permite auditar de forma reproducible los axiomas de los que depende cada teorema; y su notación es cercana a la matemática ordinaria. Además, Lean implementa el Cálculo de Construcciones Inductivas , así que es el ejemplo natural para la teoría que se reconstruye en los niveles 1 a 6 de este sitio.

La idea central, todavía sin formalismo

Todo el edificio descansa en la correspondencia de Curry–Howard , cuyo lema reza «proposiciones como tipos, pruebas como términos» (Wadler, 2015) . En una teoría de tipos , cada expresión bien formada (cada término) tiene un tipo, y la afirmación «el término $t$ tiene tipo $T$» es comprobable por un procedimiento sintáctico. La correspondencia asigna a cada proposición $P$ un tipo cuyos términos son precisamente las demostraciones de $P$. Dos consecuencias inmediatas:

Verificar una demostración se reduce, así, a comprobar el tipo de un término: una tarea sintáctica que ejecuta el núcleo del asistente. Nada de esto es formal todavía; los niveles 1 a 3 construyen ambos lados de la tabla (el cálculo lambda con tipos por un lado, la deducción natural por el otro), y el nivel 4 enuncia la correspondencia con precisión.

De ahí sale la promesa que la tesis pone a prueba: si una demostración es un término y un programa también lo es, el mismo principio debería certificar por igual un teorema de la lógica y la corrección de un algoritmo. Los dos estudios de caso (la completitud de la deducción natural clásica proposicional y la corrección de quicksort) existen exactamente para exhibir ese espectro completo.

Qué significa «verificado» (y qué no significa)

«Verificado por máquina» significa aquí una cosa precisa: aceptado por el núcleo de Lean y sus bibliotecas. La confianza no se elimina; se reduce y se reubica en tres puntos que conviene tener a la vista:

1. La corrección del núcleo. El verificador mismo podría contener errores. Es pequeño y auditable, pero es un supuesto, y la tesis lo declara como tal: la confianza última recae en la corrección de ese núcleo, atenuada (no eliminada) por los mecanismos siguientes.
2. Los axiomas declarados. Un teorema puede depender de axiomas; la auditoría de axiomas los deja a la vista, como se detalla más abajo.
3. La fidelidad del enunciado formal. El núcleo garantiza que el término demuestra el enunciado escrito, no que el enunciado escrito diga lo que uno cree. Por eso la tesis somete su formalización a una validación cruzada independiente: se comprueba que su noción de tautología coincide con la de la biblioteca Foundation del ecosistema de Lean, una confirmación externa de la que la prueba principal no depende.

Verificado tampoco significa exhaustivo. El alcance se declara con la misma precisión: la completitud se formaliza para la lógica proposicional clásica sobre el fragmento $\{\neg, \rightarrow\}$ (expresivamente adecuado, pues los demás conectivos son definibles), no para la lógica de primer orden; y de quicksort se verifica la corrección funcional (que la salida es una permutación ordenada de la entrada), no su complejidad ni sus variantes sobre arreglos: el interés está en qué calcula el algoritmo, no en cuán rápido lo hace.

La auditoría de axiomas como mecanismo de honestidad

En los dos estudios de caso se impone la misma disciplina: ninguna laguna (sorry) y ningún lema postulado. Al final, cada teorema principal se somete a la orden #print axioms, que responde con la lista exacta de axiomas de los que depende la prueba:

#print axioms quicksort_correct
-- 'quicksort_correct' depends on axioms: [propext, Classical.choice, Quot.sound]

Los tres axiomas reportados son propext (extensionalidad proposicional), Classical.choice (el axioma de elección) y Quot.sound (corrección de los cocientes): los fundamentos clásicos estándar sobre los que se construye Mathlib entero, no supuestos específicos de estos desarrollos. La tesis no persigue una formalización constructiva que los evite; lo que persigue es que los supuestos no sean materia de opinión ni de lectura cuidadosa, sino la salida de un comando reproducible. Ese es el mecanismo de honestidad: el resultado declara públicamente sobre qué descansa.

La ruta de aquí en adelante

El resto del sitio recorre, en ocho niveles, el camino que va de la teoría a los dos resultados verificados:

• Niveles 1 y 2: el cálculo lambda no tipado (sintaxis, sustitución, β-reducción, formas normales y confluencia) y los tipos simples.
• Nivel 3: la lógica proposicional: deducción natural, semántica de tablas, solidez y el argumento de Kalmár .
• Nivel 4: la correspondencia de Curry–Howard, ya con toda precisión.
• Nivel 5: el cubo-λ, tres formas de dependencia y su combinación en el Cálculo de Construcciones.
• Nivel 6: el CIC y Lean: tipos inductivos , recursores , universos y tácticas.
• Niveles 7 y 8: los dos estudios de caso completos, definición por definición y lema por lema, incluida la terminación de quicksort por recursión bien fundamentada y las auditorías finales.

En todos ellos se sigue la metodología dual de la tesis: cada resultado aparece primero como matemática ordinaria, con su demostración, y luego como su realización en Lean, línea por línea, conservando la estructura del argumento. El punto de partida es el cálculo lambda: allí comienza el nivel 1.