Sobre la tesis

Esta guía es la adaptación interactiva de la tesis de licenciatura en matemática aplicada «Aplicación de Lean en el desarrollo de pruebas matemáticas» (Universidad del Valle de Guatemala), que estudia los fundamentos del asistente de pruebas Lean 4 y los pone a prueba con dos formalizaciones completas:

• el teorema de completitud de la deducción natural clásica proposicional, demostrado de manera interna mediante una realización constructiva del lema de Kalmár, y
• la corrección del algoritmo quicksort: la salida es una permutación ordenada de la entrada.

Ninguna de las dos usa sorry ni lemas postulados, y ambas pasan una auditoría de axiomas (#print axioms) que certifica exactamente en qué supuestos descansan.

El código verificado

Todo el desarrollo Lean es público y compila de principio a fin, con la versión del compilador fijada (leanprover/lean4:v4.29.0) y comprobado en integración continua:

github.com/RudiksChess/lean_execution

Los listados que aparecerán en los módulos experto (completitud y quicksort) son extractos textuales de ese repositorio, con enlace al archivo exacto.

Validación cruzada

Además de la auditoría de axiomas, la tesis valida sus resultados por dos vías independientes:

• La biblioteca Foundation (FormalizedFormalLogic): un puente formal (BridgeToFoundation.lean) comprueba que la noción de tautología del desarrollo coincide con la de esa biblioteca, sin que la prueba principal dependa de ella.
• Harmonic Aristotle (apéndice de la tesis): a un agente independiente se le dio solo la sintaxis, la semántica y el cálculo (sin el lema de Kalmár ni la construcción de descarga), y reconstruyó el teorema de completitud completo, redescubriendo el método por su cuenta; con solo la definición de quicksort reconstruyó también su corrección. Ambas reconstrucciones convergen a los mismos teoremas con la misma auditoría de axiomas (propext, Classical.choice, Quot.sound, sin sorryAx) y viven en la carpeta aristotle/ del repositorio.

Esta guía

La guía reordena el material de la tesis en una ruta pedagógica de nueve niveles y añade componentes interactivos (reducción β paso a paso, tablas de verdad, derivaciones desplegables) cuyos motores están programados siguiendo las definiciones exactas del texto y verificados con pruebas automatizadas. La numeración de definiciones y teoremas se conserva para que cada afirmación pueda contrastarse con el documento original.