¿Por qué usa Lean Dependent Type Theory?
¡Hola Oriol! Buena pregunta. Lean usa teoría de tipos dependientes por varias razones de fondo.
La idea central es que en los tipos dependientes un tipo puede depender de un valor. Esto te permite expresar proposiciones matemáticas directamente como tipos, gracias a la correspondencia de Curry-Howard: una demostración de un teorema es, literalmente, un término de cierto tipo. Así, comprobar que una prueba es correcta se reduce a comprobar que un tipo encaja, algo que el núcleo de Lean puede verificar de forma pequeña y fiable.
En concreto, Lean usa una variante llamada Teoría de Tipos Inductivos con un universo impredicativo de proposiciones, lo que le da a la vez mucha expresividad y un núcleo de confianza bastante compacto. ¿Quieres que entre en cómo se compara con el Cálculo de Construcciones de Coq, o con enfoques más basados en teoría de conjuntos?
¿Por qué es importante que sea una teoría de tipos dependientes? ¿Qué aporta?
Buena pregunta, y toca el corazón del asunto. Lo que aportan los tipos dependientes frente a sistemas de tipos normales es poder meter valores dentro de los tipos, y eso desbloquea tres cosas clave.
Primero, puedes expresar especificaciones precisas. En vez de hablar solo de “una lista”, puedes hablar de “una lista de longitud n”, y el tipo mismo garantiza esa propiedad. Las restricciones que normalmente verificarías en tiempo de ejecución pasan a estar codificadas en el tipo y comprobadas por el verificador.
Segundo, y es lo fundamental para un asistente de demostraciones, te permite representar proposiciones lógicas como tipos mediante Curry-Howard. Sin dependencia solo podrías capturar lógica proposicional bastante pobre. Con tipos dependientes, el cuantificador “para todo” se corresponde con el tipo producto dependiente, y “existe” con el tipo suma dependiente. Es decir, obtienes lógica de primer orden y de orden superior de forma nativa, sin añadir un sistema lógico aparte.
Y tercero, unifica en un solo lenguaje los datos, los programas y las pruebas. Una demostración es un término, un programa es un término, y ambos se comprueban con las mismas reglas. Eso da una base conceptual muy económica.
¿Te interesa más el lado lógico, el de verificación de programas, o cómo se traduce esto en la práctica al escribir pruebas en Lean?
¿Se usa como lenguaje de programación?
¿Cuál es su performance comparada con Haskell o con C?
Sí, Lean 4 es un lenguaje de programación de propósito general de verdad, no solo un asistente de demostraciones. De hecho, buena parte del propio Lean 4 está escrito en Lean. Eso fue un cambio importante respecto a Lean 3.
Sobre el rendimiento, déjame darte el panorama honesto, aunque esto es terreno donde las comparaciones precisas dependen mucho del benchmark.
Frente a Haskell, están en una liga parecida. Ambos son funcionales, compilan a código nativo, y Lean usa una estrategia interesante de conteo de referencias con una optimización llamada reutilización destructiva, a veces apodada paradigma funcional pero in-place. Esa técnica detecta cuándo un objeto tiene una sola referencia y reutiliza su memoria en lugar de reasignar, lo que ayuda mucho en código funcional. En algunos casos Lean iguala o supera a Haskell; en otros Haskell gana por su recolector de basura más maduro y décadas de optimización del compilador.
Frente a C, C sigue ganando claramente en rendimiento bruto. Lean no te da control manual de memoria, tiene el coste del conteo de referencias, y el runtime hace boxing de muchos valores. Para cálculo numérico intensivo o código de sistemas de bajo nivel, C está en otro nivel.
La forma justa de verlo es que Lean apunta a ser lo bastante rápido para su propio compilador y herramientas, no a competir con C. ¿Quieres que mire benchmarks concretos y actuales, o te interesa más cómo funciona ese modelo de memoria por dentro?
Compáralo con Python.
Ah, ahí la comparación cambia bastante a favor de Lean. Lean 4 es considerablemente más rápido que Python en casi cualquier cosa computacional.
La razón de fondo es que Lean compila a código nativo a través de C, mientras que CPython interpreta bytecode. Para bucles, recursión y cálculo con enteros, Lean suele estar uno o dos órdenes de magnitud por delante, es decir, decenas o cientos de veces más rápido en los casos típicos. Además Lean tiene tipado estático, así que no paga el coste de resolver tipos en tiempo de ejecución que lastra a Python.
Dicho esto, hay matices. Mucho código Python pesado en realidad llama por debajo a bibliotecas en C o Fortran, como NumPy, y ahí la comparación ya no es Python puro contra Lean, sino C contra Lean. Y Python gana por goleada en otra dimensión que no es velocidad: ecosistema, librerías, y lo rápido que escribes y prototipas.
Así que yo lo resumiría como que Lean te da seguridad de tipos muy fuerte y rendimiento nativo, mientras que Python te da velocidad de desarrollo y un ecosistema enorme. Son herramientas para propósitos bastante distintos. ¿Lo estás comparando con algún uso concreto en mente?
Dame un ejemplo de software desarrollado con Lean. Eh,
Hmm, aquí tengo que ser honesto contigo: el ejemplo más claro y sólido es el propio Lean. El compilador de Lean 4 y su biblioteca estándar están escritos en Lean, y eso es software real y considerable que se autoalberga, lo cual ya es una prueba de fuego seria para un lenguaje.
Más allá de eso, el ecosistema de software de propósito general hecho en Lean todavía es pequeño y joven. Lo que sí es grande es el lado matemático: Mathlib, una biblioteca enorme de matemática formalizada, con cientos de miles de teoremas. Y ha habido proyectos de formalización muy sonados, como el Liquid Tensor Experiment de Peter Scholze, que verificó un teorema de investigación puntero.
Pero déjame no fiarme solo de mi memoria aquí, porque en aplicaciones concretas y recientes podría estar desactualizado. ¿Quieres que busque ejemplos actuales de software o proyectos notables construidos con Lean?
Hazlo. Hazlo.
Déjame buscar ejemplos actuales. Perfecto, esto confirma y amplía bastante el panorama. Te doy ejemplos concretos.
En verificación de software real, hay uno destacado: Microsoft Research usa Lean, a través de una herramienta llamada Aeneas, para verificar formalmente algoritmos criptográficos de producción en SymCrypt, que es la biblioteca de criptografía de Windows. Eso es software en producción, no un experimento académico. En esa misma línea, Amazon ha hecho la mayor donación de su historia a la fundación de Lean, precisamente por su interés en razonamiento automático para verificación.
Luego hay un ecosistema emergente de aplicaciones reales, aunque todavía modesto: hay implementaciones estilo producción de la clásica aplicación TodoMVC con autenticación y despliegue en AWS Lambda, un gestor de entornos de Python escrito en Lean llamado viper, servicios con gRPC y PostgreSQL, e incluso cosas lúdicas como un motor de raycasting tipo Doom usando SDL3 y ajedrez en Lean.
Y en el lado de la inteligencia artificial para matemáticas, sistemas punteros como AlphaProof de DeepMind y la serie DeepSeek-Prover generan sus demostraciones en Lean 4.
Así que el resumen se mantiene: el buque insignia sigue siendo el propio compilador de Lean, lo más masivo es Mathlib y la formalización matemática, pero ya está empezando a aparecer software de propósito general y, muy notablemente, verificación de criptografía de producción. ¿Te interesa alguno en particular?
¿La IA te puede ayudar a escribir software en Lean?
Sí, bastante, y de hecho es un área muy activa ahora mismo. Pero conviene separar dos cosas que la IA hace con Lean, porque son distintas.
La primera es demostración automática de teoremas, que es donde la IA está más madura. Sistemas como AlphaProof de DeepMind o DeepSeek-Prover se entrenan específicamente para generar pruebas en Lean, y aprovechan algo muy potente: el verificador de Lean actúa como un juez infalible. La IA propone una prueba, Lean la comprueba, y si está mal da error. Ese bucle de retroalimentación cierra la puerta a las alucinaciones, porque una prueba o pasa el verificador o no pasa. Eso hace de Lean un terreno ideal para la IA, mucho más que lenguajes normales.
La segunda es escribir código Lean de propósito general, como escribirías Python o Rust. Ahí la IA ayuda, pero con más limitaciones. El motivo es simple: hay muchísimo menos código Lean en el mundo que Python o JavaScript, así que los modelos han visto menos ejemplos y cometen más errores, sobre todo con sintaxis de Lean 4, que cambió respecto a Lean 3 y a veces los modelos los mezclan.
Ahora bien, hay una sinergia bonita aquí. Si escribes código con especificaciones formales, la IA puede generar el código y además la prueba de que es correcto, y el verificador comprueba ambas cosas. Esa idea, a veces llamada verified code generation, es justo hacia donde apuntan varios proyectos que vi, con benchmarks dedicados. Es probablemente el futuro más interesante: IA que no solo escribe software, sino que demuestra que hace lo que debe.
¿Lo preguntas porque estás pensando en meterte con Lean tú mismo?
¿Haskell tiene alguna extensión con dependent types?
Sí, aunque con matices importantes. Haskell no tiene tipos dependientes plenos como Lean, pero lleva años acercándose a ellos a base de extensiones del compilador GHC.
Históricamente, la forma de simular dependencia era mediante varias extensiones combinadas. Las principales son GADTs, que son tipos de datos algebraicos generalizados, los type families, que son como funciones a nivel de tipos, y DataKinds, que te permite promover valores al nivel de tipos. Con esas tres combinadas puedes hacer buena parte de lo que harías con dependencia, por ejemplo las famosas listas con longitud en el tipo, los vectores por tamaño. Pero es verboso y a menudo tienes que usar singletons, un truco para tender un puente entre el mundo de los valores y el de los tipos, porque en Haskell esos dos mundos están separados.
Y aquí está la novedad grande: hay un esfuerzo en marcha para traer dependencia de verdad a Haskell, conocido como Dependent Haskell. Ya ha aterrizado una pieza clave, la extensión que permite explícitamente cuantificar sobre tipos de forma visible, y el trabajo de Richard Eisenberg y otros apunta a unificar poco a poco el nivel de términos y el de tipos.
La diferencia de fondo con Lean es filosófica. Haskell añade dependencia sobre un lenguaje que no fue diseñado para ella, así que separa tiempo de compilación y ejecución y arrastra esa dualidad. Lean parte de la teoría de tipos dependientes desde el primer día, así que todo es uniforme. Por eso en Lean la dependencia se siente natural y en Haskell se siente, digamos, injertada, aunque funciona.
¿Quieres que entre en cómo funcionan los singletons, o en qué le falta aún a Dependent Haskell para estar completo?