Hola.
¡Hola, Oriol! ¿En qué te puedo ayudar hoy?
Estaba pensando en aprender Lean para
¡Ah, Lean! Buena elección si te va la matemática formal y la demostración asistida por ordenador. ¿Para qué lo quieres aprender, formalizar matemáticas o más bien verificación de software?
y para el algo de la matemática. Sí, claro, claro. Lo quiero aprender para formalizar matemáticas.
Genial. Entonces el camino casi obligado es Lean 4 con Mathlib, que es la gran biblioteca de matemática formalizada.
El recurso estrella para empezar es el “Natural Number Game”, un juego interactivo donde demuestras teoremas sobre números naturales desde cero. Es adictivo y te enseña la mecánica de las tácticas sin instalar nada. Después, el libro “Mathematics in Lean” te lleva ya a cosas más serias usando Mathlib.
¿Quieres que te prepare una ruta de aprendizaje más detallada, o prefieres empezar por lo básico y me preguntas según avances?
para conocer cómo funciona, qué puede hacer, lo que no. Y me interesa sobre todo
Perfecto, dime, ¿sobre todo qué? Te quedaste a medias. ¿Te interesa sobre todo entender hasta dónde llega, qué tipo de matemática se puede formalizar, o algo más concreto?
Que se demuestre No, no, no. Me interesa que busques algún ejemplo de teorema matemático.
¿Quieres que busque algún ejemplo concreto de un teorema matemático importante que ya se haya formalizado en Lean? Por ejemplo, hay casos famosos como el teorema de los números primos, o trabajos recientes de Terence Tao. Déjame buscarlo bien para darte ejemplos reales y actuales. Perfecto, encontré ejemplos buenísimos y además muy actuales. Mira:
Hay una lista famosa de cien teoremas clásicos que sirve para comparar asistentes de demostración, y en Lean ya están formalizados ochenta y cinco de esos cien. Ahí entran clásicos como la infinitud de los números primos, la irracionalidad de raíz de dos o el teorema fundamental del cálculo.
Pero lo más impresionante son los proyectos de frontera. Terence Tao lideró la formalización de la conjetura polinomial de Freiman-Ruzsa. Está también el “Liquid Tensor Experiment”, donde se verificó un resultado durísimo de Peter Scholze. Y ahora mismo hay un proyecto en marcha para formalizar nada menos que el Último Teorema de Fermat.
Y un dato muy reciente: hace unos días, el nueve de octubre, Tao publicó un artículo sobre qué deberían saber los matemáticos de Lean, fiabilidad e inteligencia artificial. ¿Quieres que te lo resuma?
de demostraciones de teoremas clásicos
Claro. Te cuento algunos de los que están en esa lista de cien y cómo se ven en Lean.
La infinitud de los números primos es el ejemplo clásico de iniciación. La demostración de Euclides se formaliza en apenas unas líneas, y en Mathlib existe como un teorema llamado, más o menos, “exists infinito primos”.
La irracionalidad de raíz de dos es otro favorito. Captura muy bien el razonamiento por contradicción y el uso de la paridad.
Luego ya hay piezas más gordas y bonitas. El teorema fundamental del álgebra, que todo polinomio complejo tiene una raíz. La ley de reciprocidad cuadrática de Gauss. El teorema de los cuatro colores. Y el teorema fundamental del cálculo, que conecta derivadas e integrales.
¿Quieres que me meta en uno concreto y te enseñe de verdad cómo luce la demostración en Lean, con sus tácticas y todo?
Me gustaría que buscases un tutorial digamos paso a paso eh, para aprender a demostrar uno de esos teoremas
Buena idea. Dado que te interesa aprender a demostrar de verdad, déjame buscar un tutorial paso a paso bien hecho, idealmente sobre algo clásico como la irracionalidad de raíz de dos o la infinitud de los primos. Encontré justo lo que buscas. Te destaco las dos mejores opciones.
La más oficial y completa es el capítulo cinco de “Mathematics in Lean”, que se titula Teoría Elemental de Números. Arranca precisamente con la irracionalidad de raíz de dos, paso a paso, y luego pasa a la infinitud de los primos. Lo bueno es que está pensado como tutorial: explica cada táctica a medida que la necesitas, y tiene ejercicios intercalados.
Y hay una joya en GitHub, un repositorio de prácticas que tiene un archivo dedicado a raíz de dos, demostrado desde cero y comentadísimo línea a línea. Además termina con dos ejercicios, demostrar que raíz de tres es irracional, y luego raíz de cualquier primo, para que practiques tú solo.
Mi recomendación sería: haz primero el “Natural Number Game” para coger soltura con las tácticas, y luego métete en ese capítulo cinco con raíz de dos. ¿Quieres que te guíe yo mismo por la demostración de raíz de dos ahora, explicándote la estrategia antes de que toques el código?
gustaría me gustaría que buscas
Perdona, te cortaste. ¿Qué te gustaría que buscase?
es otro tutorial hecho por alguien que me envía el link
Ah, entiendo. ¿Quieres que busque otro tutorial, uno hecho por algún particular, como una entrada de blog o un vídeo, y que te pase el enlace directo? Déjame buscar. Hay uno que encaja perfecto con lo que pides, un tutorial de blog hecho por un particular. Se titula “My First Lean 4 Proof: the Irrationality of root 2”, en el sitio Architecture and Performance. Lo bonito es justo ese enfoque: alguien contando su primera demostración en Lean 4 desde cero, paso a paso, explicando cómo piensa.
El enlace es architecture dash performance punto fr, y luego la ruta del blog sobre esa primera demostración en Lean 4. Como es un enlace largo con guiones, si quieres te lo dejo escrito limpio en el chat de texto para que puedas copiarlo y pegarlo sin errores.
¿Te viene bien así, o prefieres que busque también algún vídeo en YouTube?
Viene bien.
Perfecto. ¿Algo más en lo que te pueda ayudar con Lean, o lo dejamos aquí por ahora?
¿Me oyes?
Sí, te oigo perfectamente. ¿Qué necesitas?
Me gustaría que buscases otro tutorial de Lean hecho por algún…
Te volviste a cortar justo al final. ¿Un tutorial de Lean hecho por algún… quién? ¿Alguna universidad, algún matemático conocido, algún youtuber? Dime y lo busco.
¿Se me oye?
Sí, se te oye bien. Me quedé esperando el final de tu frase: querías otro tutorial de Lean hecho por algún… ¿quién?
Yo por un particular. Busca un tutorial de Lean hecho por un particular.
Déjame buscar otro tutorial de Lean hecho por un particular, distinto al del blog que ya te pasé. Encontré un par muy buenos de particulares. Te menciono los dos que más me gustan.
Uno es de Brandon Rozek, en su blog personal. Se titula simplemente “Lean 4 Tutorial”. Él mismo cuenta que es una versión actualizada de uno que hizo antes para Lean 3, con la sintaxis al día, y va construyendo pruebas desde lo más básico.
Y el otro, que me parece una joya para entender cómo se leen las demostraciones, es “The Hitchhiker’s Guide to Reading Lean 4 Theorems”, en el blog de Lambdaclass. Ese es buenísimo porque te explica el modo táctico como si fuera una sesión de depuración, con el estado de la prueba anotado en cada paso.
¿Quieres que te deje los enlaces limpios de estos dos en el chat de texto, igual que el anterior?
Genera un artefacto con toda esta información.
Buena idea. Como el artefacto conviene guardarlo también en tu carpeta de Drive, déjame comprobar primero las herramientas que necesito para crearlo y guardarlo allí. Ya tengo lo que necesito. El artefacto, una guía con todos estos recursos para aprender Lean, lo mejor es que lo prepare y lo veas en el chat de texto, porque lleva enlaces y fragmentos de código que no tienen sentido leídos en voz alta. Además lo guardaré en tu carpeta “Claude Artifacts” de Drive.
Voy a crearlo ahora con todo: la ruta de aprendizaje, los teoremas clásicos de ejemplo, y los tres tutoriales de particulares que encontramos. ¡Listo! Lo tienes todo en un documento llamado “Aprender Lean 4 - Guía y recursos”, guardado en tu carpeta “Claude Artifacts” de Drive.
Incluye la ruta de aprendizaje, qué puede hacer Lean y hasta dónde llega, los teoremas clásicos de ejemplo, y los tutoriales de particulares, con todos los enlaces limpios para que los puedas pinchar. ¿Algo más?
Según entiendo, Lean 4 está basado en el cálculo de construcciones y
Exacto, vas muy bien encaminado. Lean 4 está basado en el Cálculo de Construcciones, en su versión con inductivos, lo que se llama el Cálculo de Construcciones Inductivas. Es una teoría de tipos dependientes.
¿Querías ir a algún punto concreto con eso, por ejemplo cómo se relaciona con el universo de proposiciones, o lo de la correspondencia de Curry-Howard? Te quedaste a mitad otra vez.
conductivas. Me gustaría que encontrases también algún tutorial sobre esto.
Vale, un tutorial que entre de verdad en los fundamentos teóricos, el Cálculo de Construcciones Inductivas y la teoría de tipos dependientes detrás de Lean. Déjame buscarlo. Encontré material muy bueno para los fundamentos. Te destaco lo mejor según lo que quieras.
Lo más directo y conectado con Lean son los capítulos dos y tres de “Theorem Proving in Lean 4”: Teoría de Tipos Dependientes, y Proposiciones y Demostraciones. Ese segundo explica justo lo que mencionabas, cómo la implicación es una función, el enfoque del Cálculo de Construcciones, y la correspondencia de Curry-Howard, el paradigma de las proposiciones como tipos.
Y hay dos joyas más teóricas. Una es “A Tour of Type Theory”, unas diapositivas de la Universidad de Colorado que construyen el Cálculo de Construcciones Inductivas desde el lambda cálculo tipado, con la sintaxis y las reglas de tipado. Y la otra, muy interesante, es un trabajo de fin de grado reciente, de noviembre de dos mil veinticinco, que cubre exactamente el Cálculo de Construcciones Inductivas y Curry-Howard aplicados a Lean 4.
¿Quiero añadir estos al mismo documento de Drive para que lo tengas todo junto?
Busca algún vídeo tutorial, guarda todo en el drive, busca algún vídeo tutorial que adicional sobre el cálculo de construcción.
Perfecto. Busco un vídeo tutorial sobre el Cálculo de Construcciones y luego lo añado todo al documento de Drive. Encontré un vídeo que encaja muy bien. Se titula “What are dependent types, aka the Calculus of Construction”, en YouTube. Es un tutorial accesible que explica los tipos dependientes y el Cálculo de Construcciones de forma didáctica, con ejemplos, sin ser una charla académica densa.
Hay otros en YouTube, pero son más de conferencia de investigación, bastante técnicos y específicos. Para aprender, el que te digo es el más apropiado.
Ahora lo añado todo al documento de Drive, los tutoriales de fundamentos y este vídeo. Un momento. Déjame recuperar la herramienta para actualizar el documento. Un momento. Esas herramientas no son las adecuadas para editar este documento de Google Docs. Déjame cargar la correcta para actualizarlo. Ya tengo la herramienta correcta. Añado al final del documento la sección de fundamentos y el vídeo. Ah, me he topado con un problema. El documento se creó bien en tu carpeta de Drive, pero para editarlo con la herramienta de Google Docs me pide volver a autenticar la conexión, y ahora mismo no puedo escribir en él.
Tienes dos opciones: o reconectas Google Docs desde los ajustes de conexiones y lo reintento, o te genero un documento nuevo, completo, con todo incluido, los fundamentos y el vídeo, y lo guardo en la carpeta. ¿Qué prefieres?
Genera uno nuevo, es fácil.
Perfecto, genero uno nuevo con todo incluido. Déjame cargar la herramienta de crear archivos en Drive. Ahora creo el documento completo en la carpeta de Drive. Listo. Ya tienes el documento nuevo en tu carpeta “Claude Artifacts”, con las seis secciones completas, incluyendo los fundamentos del Cálculo de Construcciones y el vídeo tutorial de YouTube al final. ¿Algo más?
Hay algún tutorial en video?añádelo al documento
Busco tutoriales en vídeo de Lean 4 y los añado al documento. Sí. Como el conector de Google Docs sigue sin autenticar y no puedo editar el documento existente, he creado una versión nueva, “Aprender Lean 4 - Guía y recursos (v2, con vídeos)”, en tu carpeta “Claude Artifacts”. Contiene todo lo anterior más una sección 7 de vídeos:
Ahora tienes tres versiones del documento en la carpeta. ¿Quieres que mueva las dos antiguas a la papelera?
Si
He movido a la papelera la versión del 12 de octubre que tenía las seis secciones. La más antigua, la que se quedó incompleta, no la he podido borrar porque Drive me ha denegado el permiso. Tendrás que eliminarla tú desde Drive: se llama igual, “Aprender Lean 4 - Guía y recursos”, sin “v2”.
Así la única versión buena es la “v2, con vídeos”.