Demostración de teoremas
Una demostración es un programa y un teorema es un tipo. Esta serie construye esa idea desde Curry-Howard hasta un pequeño demostrador en Python, un mini-Lean en Julia y demostraciones reales en Lean 4.
Sobre la imagen Colossus ponía a prueba hipótesis lógicas sobre la configuración de los cifrados alemanes de forma mecánica y a gran velocidad. Es un caso temprano de la idea detrás de esta serie: un razonamiento escrito con la precisión suficiente para que una máquina lo verifique. Una computadora para descifrar códigos Colossus Mark 2 en Bletchley Park, operada por dos integrantes del Women’s Royal Naval Service, 1944 o 1945. Foto: fotógrafo desconocido, The National Archives (Reino Unido), dominio público, vía Wikimedia Commons.
Traducción automática del original en inglés, todavía sin revisar. Leer el original.
Una demostración es un programa. Un teorema es un tipo. Una vez que lo ves no lo podés dejar de ver, y mucho de lo que parecen dos campos separados resulta ser un solo campo fotografiado desde dos lados.
La mayoría de la gente que escucha hablar de la correspondencia de Curry-Howard la archiva como una curiosidad. Es la razón por la que un demostrador de teoremas (theorem prover) moderno tiene estructuralmente la misma forma que un pequeño compilador funcional. Un núcleo confiable chiquito. Un puñado de axiomas. Un type checker haciendo aritmética sobre proposiciones. Todo lo demás es azúcar encima.
La serie construye la idea de cuatro maneras:
- Las proposiciones son tipos. Qué dice realmente Curry-Howard, y por qué cambia cómo leés tanto programas como demostraciones.
- Un pequeño demostrador en Python. Un lenguaje de términos, un verificador y un kernel de confianza, escritos de forma explícita para que la arquitectura no se pueda esconder.
- Un mini-Lean en Julia. Guillermo Angeris mete un demostrador que funciona en 61 líneas de Julia apoyándose en el sistema de tipos. Seis axiomas, y el compilador hace el resto.
- Escribir demostraciones en Lean. Los mismos tres teoremas del demostrador en Python, ahora en Lean 4. La versión que realmente usás.
Curry y Howard notaron el patrón. Martin-Löf construyó una lógica a partir de él. Lean es donde vive hoy. Empezá por el principio si querés la idea primero; empezá por el episodio dos si preferís ver la construcción y dejar que la idea salga sola.
Episodios
-
Episodio 1: Las proposiciones son tipos, las demostraciones son programas
La correspondencia de Curry-Howard dice que los tipos y las proposiciones lógicas son lo mismo. Entender por qué cambia cómo pensás tanto la programación como la matemática.
-
Episodio 2: Construyendo un pequeño demostrador de teoremas en Python
Un pequeño demostrador de teoremas es apenas un lenguaje de términos, un checker y un kernel chico de confianza. Construimos uno en Python puro para dejar la arquitectura a la vista.
-
Episodio 3: Programar un mini-Lean en el sistema de tipos de Julia
Guillermo Angeris arma un demostrador de teoremas que funciona en 61 líneas de Julia. Un kernel de confianza chiquito, seis axiomas, y el compilador hace el resto. Esta es la construcción.
-
Episodio 4: Tus primeras demostraciones en Lean
Los mismos tres teoremas del demostrador en Python, ahora en Lean 4.